proposition: Lemma AntiMesh_nonneg : forall n (a b : IR) (Hab : a [<=] b) (P : Partition Hab n), [0] [<=] AntiMesh P.
proof: Proof. intro; induction n as [| n Hrecn]. intros; unfold AntiMesh in |- *; simpl in |- *. apply leEq_reflexive. intros. unfold AntiMesh in |- *. apply leEq_minlist. simpl in |- *; auto with arith. intros y H. simpl in H; elim H; clear H; intro H0. unfold AntiMesh in Hrecn. apply leEq_transitive with (minlist (Part_Mesh_List (Partition_Dom P))). 2: apply minlist_smaller; assumption. apply Hrecn. eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply H0. apply shift_leEq_minus; astepl (P _ (le_S _ _ (le_n n))). apply prf2. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)