proposition: Lemma lip_modulus_pos (L e : Q) : 0 ≤ L -> 0 < e -> 0 < lip_modulus L e.
proof: Proof. intros L_nonneg e_pos. unfold lip_modulus. destruct (decide (L = 0)) as [A1 | A1]; [apply I |]. apply not_symmetry in A1. change (0 < e / L). assert (0 < L) by now apply QOrder.le_neq_lt. Qauto_pos. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.QArith MathClasses.theory.setoids MathClasses.theory.products MathClasses.implementations.stdlib_rationals MathClasses.interfaces.abstract_algebra MathClasses.implementations.QType_rationals MathClasses.interfaces.additional_operations CoRN.tactics.Qauto Coq.QArith.QOrderedType MathClasses.theory.rings MathClasses.theory.dec_fields MathClasses.orders.rings MathClasses.orders.dec_fields MathClasses.theory.nat_pow MathClasses.interfaces.naturals MathClasses.interfaces.orders CoRN.reals.fast.CRGeometricSum