proposition: Lemma Rlinear_non_zero_2:forall a b x y, (y<>0)%R -> (a*(x/y)+b<>0)%R -> (a*x+b*y<>0)%R.
proof: Proof. intros a b x y Hy Habxy. stepl (y*(a*(x/y)+b))%R; auto; field; auto. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)