proposition: Lemma separation_conseq : forall (j : nat) (Hj : j <= m), AbsIR (P i Hi[-]R j Hj)[<]delta [/]TwoNZ -> forall j' : nat, j <> j' -> forall Hj' : j' <= m, delta [/]TwoNZ[<]AbsIR (P i Hi[-]R j' Hj').
proof: Proof. intros j Hj H; intros. elim (Cnat_total_order _ _ H0); clear H0; intro H0. elim (le_lt_dec j' m); intro. cut (S j <= m); [ intro | clear H; apply Nat.le_trans with j'; auto ]. eapply less_wdr. 2: apply AbsIR_minus. cut (R (S j) H1[<=]R j' Hj'); intros. eapply less_wdr. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. rstepr (R _ Hj'[-]R _ H1[+](R _ H1[-]R _ Hj)[+](R _ Hj[-]P i Hi)). rstepl ([0][+]delta[+][--](delta [/]TwoNZ)). apply plus_resp_leEq_less. apply plus_resp_leEq_both. apply shift_leEq_minus; astepl (R _ H1). assumption. apply leEq_transitive with deltaR. apply RS_delta_deltaR. unfold deltaR in |- *; apply AntiMesh_lemma. rstepl ([--](delta [/]TwoNZ)). rstepr ([--](P i Hi[-]R j Hj)). apply inv_resp_less. eapply leEq_less_trans. apply leEq_AbsIR. assumption. apply shift_leEq_minus; astepl (P i Hi). eapply leEq_transitive. 2: apply H2. apply less_leEq; apply less_transitive_unfolded with (R j Hj[+]delta [/]TwoNZ). apply shift_less_plus'. eapply leEq_less_trans; [ apply leEq_AbsIR | apply H ]. apply shift_plus_less'. apply less_leEq_trans with delta. apply pos_div_two'; exact RS_delta_pos. apply leEq_transitive with deltaR. apply RS_delta_deltaR. unfold deltaR in |- *; apply AntiMesh_lemma. apply local_mon_imp_mon'_le with (f := fun (i : nat) (Hi : i <= m) => R i Hi). intros; apply HR. red in |- *; intros; apply prf1; auto. assumption. exfalso; apply (Nat.le_ngt j' m); auto. elim (le_lt_dec j 0); intro. exfalso; apply Nat.nlt_0_r with j'; red in |- *; apply Nat.le_trans with j; auto. generalize Hj H H0; clear H0 H Hj. set (jj := pred j) in *. cut (j = S jj); [ intro | unfold jj in |- *; symmetry; apply Nat.lt_succ_pred with 0; auto ]. rewrite H; intros. cut (jj <= m); [ intro | auto with arith ]. cut (R j' Hj'[<=]R jj H2); intros. eapply less_wdr. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. rstepr (P i Hi[-]R _ Hj[+](R _ Hj[-]R jj H2)[+](R jj H2[-]R j' Hj')). rstepl ([--](delta [/]TwoNZ)[+]delta[+][0]). apply plus_resp_less_leEq. apply plus_resp_less_leEq. eapply less_wdr. 2: apply cg_inv_inv. apply inv_resp_less; eapply leEq_less_trans. 2: apply H0. apply inv_leEq_AbsIR. eapply leEq_transitive. apply RS_delta_deltaR. unfold deltaR in |- *; apply AntiMesh_lemma. apply shift_leEq_minus; eapply leEq_wdl. apply H3. algebra. apply shift_leEq_minus; astepl (R j' Hj'). eapply leEq_transitive. apply H3. apply less_leEq; apply less_transitive_unfolded with (R _ Hj[-]delta [/]TwoNZ). apply shift_less_minus; apply shift_plus_less'. apply less_leEq_trans with delta. apply pos_div_two'; exact RS_delta_pos. eapply leEq_transitive. apply RS_delta_deltaR. unfold deltaR in |- *; apply AntiMesh_lemma. apply shift_minus_less; apply shift_less_plus'. eapply leEq_less_trans. 2: apply H0. eapply leEq_wdr. 2: apply AbsIR_minus. apply leEq_AbsIR. apply local_mon_imp_mon'_le with (f := fun (i : nat) (Hi : i <= m) => R i Hi). intros; apply HR. red in |- *; intros; apply prf1; auto. auto with arith. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions