proposition: Lemma Mesh_wd' : forall n a b (Hab : a [<=] b) (P Q : Partition Hab n), (forall i Hi, P i Hi [=] Q i Hi) -> Mesh P [=] Mesh Q.
proof: Proof. intros. apply Mesh_wd. intros; apply H. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)