Changeset 2286 for src/utilities
 Timestamp:
 Aug 2, 2012, 3:18:11 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extranat.ma
r1593 r2286 108 108 @(match commutative_plus_faster n' m return λx.λ_.? = S x with [refl ⇒ ?]) @refl qed. 109 109 110 lemma distributive_times_plus_fast : distributive ? times plus. 111 #n elim n [ #m #p % ] 112 #n' #IH #m #p normalize 113 >IH 114 >associative_plus in ⊢ (???%); 115 <(associative_plus ? p) in ⊢ (???%); 116 >(commutative_plus_faster ? p) in ⊢ (???%); 117 >(associative_plus p) 118 @associative_plus 119 qed. 120 121 lemma times_n_Sm_fast : ∀n,m.n + n * m = n * S m. 122 #n elim n n 123 [ #m % ] 124 #n #IH #m normalize <IH 125 <associative_plus >(commutative_plus_faster n) 126 >associative_plus >IH % 127 qed. 128 129 lemma commutative_times_fast : commutative ? times. 130 #n elim n n 131 [ #m <times_n_O % ] 132 #n #IH #m normalize <times_n_Sm_fast >IH % 133 qed. 134
Note: See TracChangeset
for help on using the changeset viewer.