proposition: Lemma Pts_part_lemma : forall g, Points_in_Partition g -> forall i Hi, compact a b Hab (g i Hi).
proof: Proof. intros g H i H0. elim (H i H0); intros. split. eapply leEq_transitive. 2: apply a0. apply leEq_wdl with (P 0 (Nat.le_0_l _)). apply Partition_mon; auto with arith. apply start. eapply leEq_transitive. apply b0. apply leEq_wdr with (P n (le_n _)). apply Partition_mon; auto with arith. apply finish. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)