proposition: Lemma sep__sep_aux_lemma : {j : nat | {Hj : j <= m | pred1 j Hj}} or (forall (j : nat) (Hj : j <= m), pred2 j Hj).
proof: Proof. apply finite_or_elim. red in |- *; unfold pred1 in |- *; do 3 intro. rewrite H; intros H0 H' H1 Hi'. eapply less_wdl. apply H1 with (Hi' := Hi'). apply AbsIR_wd; apply cg_minus_wd; apply prf1; auto. red in |- *; unfold pred2 in |- *; intros. rename X into H1. eapply less_wdr. apply H1 with (Hi' := Hi'). apply AbsIR_wd; apply cg_minus_wd; apply prf1; auto. intros j Hj. cut (pred2 j Hj or pred1 j Hj). intro H; inversion_clear H; [ right | left ]; assumption. unfold pred1, pred2 in |- *. cut (forall Hi' : i <= n, delta [/]FourNZ[<]AbsIR (P i Hi'[-]R j Hj) or AbsIR (P i Hi'[-]R j Hj)[<]delta [/]TwoNZ). intro H. elim (le_lt_dec i n); intro. elim (H a0); intro. left; intro. eapply less_wdr. apply a1. apply AbsIR_wd; apply cg_minus_wd; apply prf1; auto. right; intro. eapply less_wdl. apply b0. apply AbsIR_wd; apply cg_minus_wd; apply prf1; auto. left; intro. exfalso; apply Nat.le_ngt with i n; auto. intros. apply less_cotransitive_unfolded. rstepl ((delta [/]TwoNZ) [/]TwoNZ). apply pos_div_two'; apply pos_div_two; apply RS_delta_pos. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions