- |#m #Hind #k generalize in match H1;cases k
- [intro;simplify in ⊢ (? (? ? (? %)) ?);simplify in ⊢ (? (? % ?) ?);
- rewrite > sym_times;rewrite < times_n_SO;apply reflexive_divides
- |intro;elim (decidable_eq_nat n2 n1)
- [rewrite > H3;rewrite < minus_n_n;
- rewrite > times_n_SO in ⊢ (? ? %);apply reflexive_divides
- |lapply (H n2)
- [lapply (H (n1 - (S n2)))
- [change in ⊢ (? ? %) with ((S n1)*n1!);
- rewrite > (plus_minus_m_m n1 n2) in ⊢ (? ? (? (? %) ?))
- [rewrite > sym_plus;
- change in ⊢ (? ? (? % ?)) with ((S n2) + (n1 - n2));
- rewrite > sym_times in \vdash (? ? %);
- rewrite > distr_times_plus in ⊢ (? ? %);
- simplify in ⊢ (? (? ? (? %)) ?);
- apply divides_plus
- [rewrite > sym_times;
- change in ⊢ (? (? ? %) ?) with ((S n2)*n2!);
- rewrite > sym_times in ⊢ (? (? ? %) ?);
- rewrite < assoc_times;
- apply divides_times
- [rewrite > sym_times;assumption
- |apply reflexive_divides]
- |rewrite < fact_minus in ⊢ (? (? ? %) ?)
- [rewrite > sym_times in ⊢ (? (? ? %) ?);
- rewrite < assoc_times;
- apply divides_times
- [rewrite < eq_plus_minus_minus_minus in Hletin1;
- [rewrite > sym_times;rewrite < minus_n_n in Hletin1;
- rewrite < plus_n_O in Hletin1;assumption
- |lapply (le_S_S_to_le ? ? H2);
- elim (le_to_or_lt_eq ? ? Hletin2);
- [assumption
- |elim (H3 H4)]
- |constructor 1]
- |apply reflexive_divides]
- |lapply (le_S_S_to_le ? ? H2);
- elim (le_to_or_lt_eq ? ? Hletin2);
- [assumption
- |elim (H3 H4)]]]
- |apply le_S_S_to_le;assumption]
- |apply le_minus_m;apply le_S_S_to_le;assumption]
- |apply le_S_S_to_le;assumption]]]]
-qed.
-
-theorem bc1: \forall n.\forall k. k < n \to bc (S n) (S k) = (bc n k) + (bc n (S k)).
-intros.unfold bc.
-rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (S k)) in ⊢ (? ? ? (? % ?))
- [rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)).
- rewrite < assoc_times in ⊢ (? ? ? (? (? ? %) ?)).
- rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (n - k)) in ⊢ (? ? ? (? ? %))
- [rewrite > assoc_times in ⊢ (? ? ? (? ? (? ? %))).
- rewrite > sym_times in ⊢ (? ? ? (? ? (? ? (? ? %)))).
- rewrite > fact_minus
- [rewrite < eq_div_plus
- [rewrite < distr_times_plus.
- simplify in ⊢ (? ? ? (? (? ? %) ?)).
- rewrite > sym_plus in ⊢ (? ? ? (? (? ? (? %)) ?)).
- rewrite < plus_minus_m_m
- [rewrite > sym_times in ⊢ (? ? ? (? % ?)).
- reflexivity
- |apply lt_to_le.
- assumption
- ]
- |rewrite > (times_n_O O).
- apply lt_times;apply lt_O_fact
- |change in ⊢ (? (? % ?) ?) with ((S k)*k!);
- rewrite < sym_times in ⊢ (? ? %);
- rewrite > assoc_times;apply divides_times
- [apply reflexive_divides
- |apply bc2;apply le_S_S_to_le;constructor 2;assumption]
- |rewrite < fact_minus
- [rewrite > sym_times in ⊢ (? (? ? %) ?);rewrite < assoc_times;
- apply divides_times
- [apply bc2;assumption
- |apply reflexive_divides]
- |assumption]]
- |assumption]
- |apply lt_to_lt_O_minus;assumption
- |rewrite > (times_n_O O).
- apply lt_times;apply lt_O_fact]
-|apply lt_O_S
-|rewrite > (times_n_O O).
- apply lt_times;apply lt_O_fact]
-qed.
-
-theorem lt_O_bc: \forall n,m. m \le n \to O < bc n m.
-intro.elim n
- [apply (le_n_O_elim ? H).
- simplify.apply le_n
- |elim (le_to_or_lt_eq ? ? H1)
- [generalize in match H2.cases m;intro
- [rewrite > bc_n_O.apply le_n
- |rewrite > bc1
- [apply (trans_le ? (bc n1 n2))
- [apply H.apply le_S_S_to_le.apply lt_to_le.assumption
- |apply le_plus_n_r
- ]
- |apply le_S_S_to_le.assumption
- ]
+ |#m #Hind #k (cases k) normalize //
+ #c #lec cases (le_to_or_lt_eq … (le_S_S_to_le …lec))
+ [#ltcm
+ cut (m-(m-(S c)) = S c) [@plus_to_minus @plus_minus_m_m //] #eqSc
+ lapply (Hind c (le_S_S_to_le … lec)) #Hc
+ lapply (Hind (m - (S c)) ?) [@le_plus_to_minus //] >eqSc #Hmc
+ >(plus_minus_m_m m c) in ⊢ (??(??(?%))); [|@le_S_S_to_le //]
+ >commutative_plus >(distributive_times_plus ? (S c))
+ @divides_plus
+ [>associative_times >(commutative_times (S c))
+ <associative_times @divides_times //
+ |<(fact_minus …ltcm) in ⊢ (?(??%)?);
+ <associative_times @divides_times //
+ >commutative_times @Hmc