proposition: Lemma length_Part_Mesh_List : forall n (a b : IR) (Hab : a [<=] b) (P : Partition Hab n), 0 < n -> 0 < length (Part_Mesh_List P).
proof: Proof. intro; case n; intros. exfalso; inversion H. simpl in |- *; auto with arith. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)