diff options
| author | coq | 2001-04-23 15:07:44 +0000 |
|---|---|---|
| committer | coq | 2001-04-23 15:07:44 +0000 |
| commit | a3837fa9dd60b7b8528e2e31c98682528c694dcd (patch) | |
| tree | 9b51b3054b6844a2f346d23a199828ba49ea8097 /theories/IntMap/Adalloc.v | |
| parent | 5993237b592c726d6777608623a7cc063b1dabb9 (diff) | |
Minor layout adjustments for Library doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1672 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/IntMap/Adalloc.v')
| -rw-r--r-- | theories/IntMap/Adalloc.v | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v index 63c2f2ad4b..ab7f19a07f 100644 --- a/theories/IntMap/Adalloc.v +++ b/theories/IntMap/Adalloc.v @@ -93,28 +93,32 @@ Section AdAlloc. Rewrite (le_antisym ? ? (nat_le_complete ? ? H) (nat_le_complete ? ? H0)). Reflexivity. Qed. - Lemma ad_le_trans : (a,b,c:ad) (ad_le a b)=true -> (ad_le b c)=true -> (ad_le a c)=true. + Lemma ad_le_trans : (a,b,c:ad) (ad_le a b)=true -> (ad_le b c)=true -> + (ad_le a c)=true. Proof. Unfold ad_le. Intros. Apply nat_le_correct. Apply le_trans with m:=(nat_of_ad b). Apply nat_le_complete. Assumption. Apply nat_le_complete. Assumption. Qed. - Lemma ad_le_lt_trans : (a,b,c:ad) (ad_le a b)=true -> (ad_le c b)=false -> (ad_le c a)=false. + Lemma ad_le_lt_trans : (a,b,c:ad) (ad_le a b)=true -> (ad_le c b)=false -> + (ad_le c a)=false. Proof. Unfold ad_le. Intros. Apply nat_le_correct_conv. Apply le_lt_trans with m:=(nat_of_ad b). Apply nat_le_complete. Assumption. Apply nat_le_complete_conv. Assumption. Qed. - Lemma ad_lt_le_trans : (a,b,c:ad) (ad_le b a)=false -> (ad_le b c)=true -> (ad_le c a)=false. + Lemma ad_lt_le_trans : (a,b,c:ad) (ad_le b a)=false -> (ad_le b c)=true -> + (ad_le c a)=false. Proof. Unfold ad_le. Intros. Apply nat_le_correct_conv. Apply lt_le_trans with m:=(nat_of_ad b). Apply nat_le_complete_conv. Assumption. Apply nat_le_complete. Assumption. Qed. - Lemma ad_lt_trans : (a,b,c:ad) (ad_le b a)=false -> (ad_le c b)=false -> (ad_le c a)=false. + Lemma ad_lt_trans : (a,b,c:ad) (ad_le b a)=false -> (ad_le c b)=false -> + (ad_le c a)=false. Proof. Unfold ad_le. Intros. Apply nat_le_correct_conv. Apply lt_trans with m:=(nat_of_ad b). Apply nat_le_complete_conv. Assumption. @@ -277,7 +281,8 @@ Section AdAlloc. Exact convert_xI. Qed. - Lemma ad_le_double_mono : (a,b:ad) (ad_le a b)=true -> (ad_le (ad_double a) (ad_double b))=true. + Lemma ad_le_double_mono : (a,b:ad) (ad_le a b)=true -> + (ad_le (ad_double a) (ad_double b))=true. Proof. Unfold ad_le. Intros. Rewrite nat_of_ad_double. Rewrite nat_of_ad_double. Apply nat_le_correct. Simpl. Apply le_plus_plus. Apply nat_le_complete. Assumption. |