proposition: Lemma Mesh_wd : forall n a b b' (Hab : a [<=] b) (Hab' : a [<=] b') (P : Partition Hab n) (Q : Partition Hab' n), (forall i Hi, P i Hi [=] Q i Hi) -> Mesh P [=] Mesh Q.
proof: Proof. simple induction n. intros. unfold Mesh in |- *; simpl in |- *; algebra. clear n; intro. case n. intros. unfold Mesh in |- *; simpl in |- *. apply cg_minus_wd; apply H0. clear n; intros. unfold Mesh in |- *. apply eq_transitive_unfolded with (Max (P _ (le_n (S (S n))) [-]P _ (le_S _ _ (le_n (S n)))) (maxlist (Part_Mesh_List (Partition_Dom P)))). simpl in |- *; algebra. apply eq_transitive_unfolded with (Max (Q _ (le_n (S (S n))) [-]Q _ (le_S _ _ (le_n (S n)))) (maxlist (Part_Mesh_List (Partition_Dom Q)))). 2: simpl in |- *; algebra. apply Max_wd_unfolded. apply cg_minus_wd; apply H0. apply eq_transitive_unfolded with (Mesh (Partition_Dom P)). unfold Mesh in |- *; algebra. apply eq_transitive_unfolded with (Mesh (Partition_Dom Q)). apply H. intros. unfold Partition_Dom in |- *; simpl in |- *. apply H0. unfold Mesh in |- *; algebra. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)