proposition: Lemma Partition_imp_points_1 : Points_in_Partition Q Partition_imp_points.
proof: Proof. red in |- *; intros. unfold Partition_imp_points in |- *; split. apply leEq_reflexive. apply prf2. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)