proposition: Lemma Rlinear_non_zero_3: forall a b x : R, a <> 0 -> x <> -b/a -> a * x + b <> 0.
proof: Proof. intros a b x Ha Hx. generalize (Rminus_eq_contra _ _ Hx); clear Hx; intros Hx. stepl (a*(x+(b/a))); [apply Rmult_resp_nonzero|field]; trivial. stepl (x - - b / a); trivial; field; trivial. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)