proposition: Lemma Partition_in_compact : forall a b Hab lng (P : Partition a b Hab lng) i Hi, compact a b Hab (P i Hi).
proof: Proof. intros. split. apply leEq_wdl with (P _ (Nat.le_0_l _)). apply Partition_mon; auto with arith. apply start. apply leEq_wdr with (P _ (le_n _)). apply Partition_mon; auto with arith. apply finish. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)