Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (8 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extralib.ma

    r1515 r1516  
    120120
    121121lemma Zmax_l: ∀x,y. x ≤ Zmax x y.
    122 #x #y whd in ⊢ (??%) lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
     122#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
    123123/3/ qed.
    124124
    125125lemma Zmax_r: ∀x,y. y ≤ Zmax x y.
    126 #x #y whd in ⊢ (??%) lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
    127 whd in ⊢ (% → ??%) /3/ qed.
     126#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
     127whd in ⊢ (% → ??%); /3/ qed.
    128128
    129129theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
     
    224224
    225225theorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
    226 #n #m #H % #H' >(Zle_to_Zleb_true … H') in H #H destruct;
     226#n #m #H % #H' >(Zle_to_Zleb_true … H') in H; #H destruct;
    227227qed.
    228228
     
    244244
    245245theorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
    246 #n #m #H % #H' >(Zlt_to_Zltb_true … H') in H #H destruct;
     246#n #m #H % #H' >(Zlt_to_Zltb_true … H') in H; #H destruct;
    247247qed.
    248248
     
    540540          lapply (partial_minus_to_Prop md'' n);
    541541          cases (partial_minus md'' n); [ 3,6,9,12: #r'' ] normalize
    542           #lt #e destruct % [ normalize /3/ | *: normalize /2/ ] @plt_pos
     542          #lt #e destruct % [ normalize /3 by le_to_le_to_eq, le_n, eq_f/ | *: normalize /2 by plt_zero, plt_pos/ ] @plt_pos
    543543          [ 1,3,5,7: @double_lt1 /2/;
    544544          | 2,4: @double_lt3 /2/;
     
    583583cases dv' in DIVIDE ⊢ %; [ 2: #dv'' ]
    584584cases md'; [ 2,4: #md'' ] #DIVIDE  normalize;
    585 >DIV in ⊢ (% → ?) #H #lt destruct;
     585>DIV in ⊢ (% → ?); #H #lt destruct;
    586586[ lapply (plus_to_minus … e0);
    587587    >(commutative_times …) >(commutative_times dv'' …)
Note: See TracChangeset for help on using the changeset viewer.