proposition: Lemma sep__part_h_lemma2 : forall (i : nat) Hi Hi', P (pred (sep__part_h (S i))) Hi'[-]P (sep__part_h i) Hi[<=]delta [/]TwoNZ.
proof: Proof. do 2 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 (j := ProjT1 a1) in *. elim (ProjT2 a1); fold j in |- *; intros Hj Hj'; elim Hj'; clear Hj'; intros H H0. change (forall Hi', P (pred j) Hi'[-]P _ Hi[<=]delta [/]TwoNZ) in |- *. intros; apply less_leEq. apply less_wdl with (P (pred j) Hi'[-]P _ a0); intros. 2: apply cg_minus_wd; apply prf1; auto. apply H0. apply Nat.lt_pred_l. apply Nat.neq_0_lt_0. apply Nat.le_lt_trans with (sep__part_h i). apply Nat.le_0_l. apply Partition_Points_mon with (P := P) (Hi := a0) (Hj := Hj). apply less_transitive_unfolded with (P (sep__part_h i) a0[+]delta [/]FourNZ). apply shift_less_plus'; astepl ZeroR; apply pos_div_four; exact RS'_delta_pos. apply shift_plus_less'; assumption. intros; eapply leEq_transitive. 2: apply less_leEq; apply b0. unfold cg_minus in |- *; apply plus_resp_leEq_both. apply Partition_mon; assumption. apply inv_resp_leEq; apply eq_imp_leEq; apply prf1; auto. exfalso; lia. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)