proposition: Lemma Mesh_lemma : forall i H H', P (S i) H'[-]P i H [<=] Mesh P.
proof: Proof. clear I; generalize n a b Hab P; clear P n Hab a b. simple induction n. intros; exfalso; inversion H'. clear n; intro m; intros. induction m as [| m Hrecm]. cut (0 = i); [ intro | inversion H'; auto; inversion H2 ]. generalize H0 H'; clear H0 H'; rewrite <- H1. intros. unfold Mesh in |- *; simpl in |- *. apply eq_imp_leEq; apply cg_minus_wd; apply prf1; auto. elim (le_lt_eq_dec _ _ H'); intro H1. cut (i <= S m); [ intro | auto with arith ]. cut (S i <= S m); [ intro | auto with arith ]. set (P' := Partition_Dom P) in *. apply leEq_wdl with (P' _ H3[-]P' _ H2). 2: simpl in |- *; apply cg_minus_wd; apply prf1; auto. apply leEq_transitive with (Mesh P'). apply H. unfold Mesh in |- *; simpl in |- *; apply rht_leEq_Max. cut (i = S m); [ intro | auto with arith ]. generalize H' H0; clear H0 H'. rewrite H2; intros. unfold Mesh in |- *; apply maxlist_greater; right. apply cg_minus_wd; apply prf1; auto. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)