Changeset 2673 for src/ASM/Util.ma


Ignore:
Timestamp:
Feb 18, 2013, 1:18:02 PM (7 years ago)
Author:
tranquil
Message:

corrected some compilation errors (that might depend on some matita update)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r2314 r2673  
    11351135qed.
    11361136
     1137(*
    11371138let rec odd_p
    11381139  (n: nat)
     
    12611262  ]
    12621263qed.
     1264*)
    12631265
    12641266lemma two_times_n_plus_one_refl_two_times_n_to_False:
    12651267  ∀m, n: nat.
    12661268    2 * m + 1 = 2 * n → False.
    1267   #m #n
    1268   #assm
    1269   cut (even_p (2 * n) ∧ even_p ((2 * m) + 1))
    1270   [1:
    1271     >assm
    1272     @conj
    1273     @two_times_n_even_p
    1274   |2:
    1275     * #_ #absurd
    1276     cases (even_p_to_not_odd_p … absurd)
    1277     #assm @assm
    1278     @two_times_n_plus_one_odd_p
    1279   ]
     1269@nat_elim2
     1270[ * [2: #n ] normalize [ <plus_n_Sm ]
     1271| #n normalize
     1272| #n #m #IH >commutative_times >commutative_times in ⊢ (???%→?); normalize
     1273] #EQ destruct @IH
     1274>commutative_times >commutative_times in ⊢ (???%); assumption
    12801275qed.
    12811276
Note: See TracChangeset for help on using the changeset viewer.