proposition: Lemma part_pred_lemma : forall a b Hab lng (P : Partition a b Hab lng) i Hi, a [<=] P i Hi.
proof: Proof. intros. apply leEq_wdl with (P 0 (Nat.le_0_l _)). apply Partition_mon; auto with arith. apply start. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)