Changeset 1516 for src/utilities/extralib.ma

Timestamp:

Nov 19, 2011, 12:38:20 AM (8 years ago)

Author:

sacerdot

Message:

Ported to syntax of Matita 0.99.1.

File:

• src/utilities/extralib.ma (modified) (5 diffs)

src/utilities/extralib.ma

@@ -120 +120 @@
 
 lemma Zmax_l: ∀x,y. x ≤ Zmax x y.
-#x #y whd in ⊢ (??%) lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
+#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
 /3/ qed.
 
 lemma Zmax_r: ∀x,y. y ≤ Zmax x y.
-#x #y whd in ⊢ (??%) lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
-whd in ⊢ (% → ??%) /3/ qed.
+#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
+whd in ⊢ (% → ??%); /3/ qed.
 
 theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
@@ -224 +224 @@
 
 theorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
-#n #m #H % #H' >(Zle_to_Zleb_true … H') in H #H destruct;
+#n #m #H % #H' >(Zle_to_Zleb_true … H') in H; #H destruct;
 qed.
 
@@ -244 +244 @@
 
 theorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
-#n #m #H % #H' >(Zlt_to_Zltb_true … H') in H #H destruct;
+#n #m #H % #H' >(Zlt_to_Zltb_true … H') in H; #H destruct;
 qed.
 
@@ -540 +540 @@
           lapply (partial_minus_to_Prop md'' n);
           cases (partial_minus md'' n); [ 3,6,9,12: #r'' ] normalize
-          #lt #e destruct % [ normalize /3/ | *: normalize /2/ ] @plt_pos
+          #lt #e destruct % [ normalize /3 by le_to_le_to_eq, le_n, eq_f/ | *: normalize /2 by plt_zero, plt_pos/ ] @plt_pos
           [ 1,3,5,7: @double_lt1 /2/;
           | 2,4: @double_lt3 /2/;
@@ -583 +583 @@
 cases dv' in DIVIDE ⊢ %; [ 2: #dv'' ]
 cases md'; [ 2,4: #md'' ] #DIVIDE  normalize;
->DIV in ⊢ (% → ?) #H #lt destruct;
+>DIV in ⊢ (% → ?); #H #lt destruct;
 [ lapply (plus_to_minus … e0);
     >(commutative_times …) >(commutative_times dv'' …)