proposition: Lemma Partition_mon : forall a b Hab lng (P : Partition a b Hab lng) i j Hi Hj, i <= j -> P i Hi [<=] P j Hj.
proof: Proof. intros; induction j as [| j Hrecj]. cut (i = 0); [ intro | auto with arith ]. apply eq_imp_leEq; apply prf1; auto. elim (le_lt_eq_dec _ _ H); intro H1. cut (j <= lng); [ intro | clear Hrecj; lia ]. apply leEq_transitive with (Pts _ _ _ _ P j H0). apply Hrecj; clear Hrecj; auto with arith. apply prf2. apply eq_imp_leEq; apply prf1; assumption. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)