proposition: Lemma Partition_Points_mon : forall n (P : Partition Hab n) i j Hi Hj, P i Hi [<] P j Hj -> i < j.
proof: Proof. intros. cut (~ j <= i); intro. apply not_ge; auto. exfalso. apply less_irreflexive_unfolded with (x := P i Hi). apply less_leEq_trans with (P j Hj). assumption. apply local_mon'_imp_mon'_le with (f := fun (i : nat) (Hi : i <= n) => P i Hi). intros; apply prf2. intro; intros; apply prf1; assumption. assumption. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)