proposition: Lemma sep__part_lemma : forall (i : nat) (Hi : i <= n), {j : nat | {Hj : j <= n | delta [/]FourNZ[<]P j Hj[-]P i Hi and (forall (j' : nat) (Hj' : j' <= n), j' < j -> P j' Hj'[-]P i Hi[<]delta [/]TwoNZ)}} or P n (le_n n)[-]P i Hi[<]delta [/]TwoNZ.
proof: Proof. intros. elim (str_finite_or_elim _ (fun (j : nat) (Hj : j <= n) => delta [/]FourNZ[<]P j Hj[-]P i Hi) (fun (j : nat) (Hj : j <= n) => P j Hj[-]P i Hi[<]delta [/]TwoNZ)); intros. left. elim a0; intros j a'. elim a'; intros Hj Hj'. elim Hj'; clear a0 a' Hj'; intros Hj' H0. exists j; exists Hj. split; assumption. right; auto. red in |- *; intros. rename X into H1. eapply less_wdr. apply H1. apply cg_minus_wd; apply prf1; auto. red in |- *; intros. rename X into H1. eapply less_wdl. apply H1. apply cg_minus_wd; apply prf1; auto. apply less_cotransitive_unfolded. apply shift_div_less. apply pos_four. rstepr (delta[+]delta). astepl ([0][+]delta). apply plus_resp_less_leEq. apply RS'_delta_pos. apply leEq_reflexive. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)