proposition: Lemma Rabs_pos_lt_contravar : forall x, 0 < Rabs x -> x <> 0.
proof: Proof. intros x Hpos ; destruct (Req_or_neq x) as [Heq | Hneq]. rewrite Heq, Rabs_R0 in Hpos ; destruct (Rlt_irrefl _ Hpos). assumption. Qed.
imports: RIneq MyNeq Rfunctions Lra