proposition: Lemma f_notequal : forall A B:Type,forall f : (A->B), forall x y :A, f x<>f y -> x<>y.
proof: Proof. intros A B f x y. apply contraposition_neg. apply f_equal. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra