proposition: Lemma Mesh_leEq : forall m (Q : Partition Hab m), Refinement P Q -> Mesh Q [<=] Mesh P.
proof: Proof. intro; case m. intros Q H. unfold Mesh at 1 in |- *; simpl in |- *. apply Mesh_nonneg. clear m; intros m Q H. unfold Mesh at 1 in |- *. apply maxlist_leEq. simpl in |- *; auto with arith. intros x H0. elim (Part_Mesh_List_lemma _ _ _ _ _ _ H0). clear H0. intros i H0. elim H0; clear H0; intros Hi H0. elim H0; clear H0; intros Hi' H0. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply H0. elim H; intros f Hf. elim Hf; clear Hf; intros Hf' Hf. cut {j : nat | {Hj : j <= n | {Hj' : S j <= n | P _ Hj [<=] Q _ Hi | Q _ Hi' [<=] P _ Hj'}}}. intro H1. elim H1; intros j Hj. elim Hj; clear H1 Hj; intros Hj Hjaux. elim Hjaux; clear Hjaux; intros Hj' Hjaux. intros HPts HPts'. apply leEq_transitive with (P _ Hj'[-]P _ Hj). unfold cg_minus in |- *; apply plus_resp_leEq_both. assumption. apply inv_resp_leEq; assumption. apply Mesh_lemma. apply Refinement_prop; assumption. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)