proposition: Lemma sep__part_h_lemma : forall i : nat, sep__part_h (S i) < n -> forall Hi Hi', P (sep__part_h i) Hi[<]P (sep__part_h (S i)) Hi'.
proof: Proof. do 3 intro; simpl in |- *. elim (le_lt_dec (sep__part_h i) n); intro; simpl in |- *. elim (sep__part_lemma (sep__part_h i) a0); intro; simpl in |- *. set (m' := ProjT1 a1) in *. change (forall Hi' : m' <= n, P (sep__part_h i) Hi[<]P m' Hi') in |- *; intros. elim (ProjT2 a1); fold m' in |- *; intros Hm' Hm''. elim Hm''; clear Hm''; intros H0 H1. apply less_transitive_unfolded with (P (sep__part_h i) Hi[+]delta [/]FourNZ). apply shift_less_plus'; astepl ZeroR; apply pos_div_four; exact RS'_delta_pos. apply shift_plus_less'; eapply less_wdr. apply H0. apply cg_minus_wd; apply prf1; auto. generalize H. simpl in |- *. elim (le_lt_dec (sep__part_h i) n); intro; simpl in |- *. elim (sep__part_lemma (sep__part_h i) a1); intro; simpl in |- *. 2: intro; exfalso; apply (Nat.lt_irrefl n); auto. 2: intro; exfalso; apply (Nat.lt_irrefl n); auto. set (m' := ProjT1 a2) in *. change (m' < n -> forall Hi' : n <= n, P (sep__part_h i) Hi[<]P n Hi') in |- *; intros. elim (ProjT2 a2); fold m' in |- *; intros Hm' Hm''. elim Hm''; clear Hm''; intros H1 H2. apply less_leEq_trans with (P _ Hm'). apply less_transitive_unfolded with (P (sep__part_h i) Hi[+]delta [/]FourNZ). apply shift_less_plus'; astepl ZeroR; apply pos_div_four; exact RS'_delta_pos. apply shift_plus_less'; eapply less_wdr. apply H1. apply cg_minus_wd; apply prf1; auto. apply local_mon'_imp_mon'2_le with (f := fun (i : nat) Hi => P i Hi). intros; apply prf2. assumption. exfalso; lia. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)