proposition: Lemma sep__part_h_lemma3 : forall (i k : nat) Hk Hk', sep__part_h i <= k -> k < pred (sep__part_h (S i)) -> P (S k) Hk'[-]P k Hk[<=]delta [/]TwoNZ.
proof: Proof. intros. cut (sep__part_h i <= n). cut (pred (sep__part_h (S i)) <= n); intros. eapply leEq_transitive. 2: apply sep__part_h_lemma2 with (Hi := H2) (Hi' := H1). unfold cg_minus in |- *; apply plus_resp_leEq_both. apply Partition_mon; assumption. apply inv_resp_leEq; apply Partition_mon; assumption. apply Nat.le_trans with (sep__part_h (S i)). auto with arith. apply sep__part_h_bnd. apply sep__part_h_bnd. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)