(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/generic_iter_p".
-
include "nat/div_and_mod_diseq.ma".
include "nat/primes.ma".
include "nat/ord.ma".
intros.
elim k
-[ rewrite < (plus_n_O n).
- simplify.
+[ simplify.
rewrite > H in \vdash (? ? ? %).
rewrite > (H1 ?).
reflexivity
rewrite > sym_plus.
rewrite > (div_plus_times ? ? ? H5).
rewrite > (mod_plus_times ? ? ? H5).
- rewrite > H4.
- simplify.reflexivity.
+ reflexivity.
]
| reflexivity
]
rewrite > sym_plus.
rewrite > (div_plus_times ? ? ? H5).
rewrite > (mod_plus_times ? ? ? H5).
- rewrite > H4.
- simplify.reflexivity.
+ reflexivity.
]
| reflexivity
]
rewrite > H8
[ reflexivity
| assumption
- | autobatch
+ | apply andb_true_true; [2: apply H12]
]
| apply eqb_false_to_not_eq.
generalize in match H14.
apply eq_f.
rewrite > sym_plus.
apply plus_minus_m_m.
- autobatch
+ autobatch by le_S_S_to_le, lt_mod_m_m, lt_O_S;
]
]
|intros.
[apply le_S_S_to_le.
change with ((i/S m) < S n).
apply (lt_times_to_lt_l m).
- apply (le_to_lt_to_lt ? i)
- [autobatch|assumption]
+ apply (le_to_lt_to_lt ? i);[2:assumption]
+ autobatch by eq_plus_to_le, div_mod, lt_O_S.
|apply le_exp
[assumption
|apply le_S_S_to_le.
[ assumption
| assumption
]
- | rewrite > H14.
+ | unfold ha.
+ unfold ha12.
+ unfold ha22.
+ rewrite > H14.
rewrite > H13.
apply sym_eq.
apply div_mod.
rewrite > Hcut.
assumption
]
- | rewrite > Hcut1.
+ | unfold ha.
+ unfold ha12.
+ rewrite > Hcut1.
rewrite > Hcut.
assumption
]
- | rewrite > Hcut1.
+ | unfold ha.
+ unfold ha22.
+ rewrite > Hcut1.
rewrite > Hcut.
assumption
]
| cut(O \lt m1)
[ cut(O \lt n1)
[ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
- [ apply (lt_plus_r).
+ [ unfold ha.
+ apply (lt_plus_r).
assumption
| rewrite > sym_plus.
rewrite > (sym_times (h11 i j) m1).
|assumption
]
]
-qed.
-
-
-
+qed.
\ No newline at end of file