proposition: Lemma contraposition_neg : forall P Q:Prop, ( P -> Q ) -> ( (~Q) -> (~P)).
proof: Proof. intros P Q hyp negQ vP. apply negQ. apply hyp. assumption. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra