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