proposition: Lemma Mesh_nonneg : forall n (a b : IR) (Hab : a [<=] b) (P : Partition Hab n), [0] [<=] Mesh P.
proof: Proof. simple induction n. intros; unfold Mesh in |- *; simpl in |- *. apply leEq_reflexive. clear n; intros. unfold Mesh in |- *. apply leEq_transitive with (P _ (le_n (S n)) [-]P _ (le_S _ _ (le_n n))). apply shift_leEq_minus; astepl (P _ (le_S _ _ (le_n n))). apply prf2. apply maxlist_greater. right; algebra. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)