proposition: Lemma R_one_zero: 1%R <> 0%R.
proof: Proof. discrR. Qed.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool Algebra_syntax Ncring Ncring_initial Ncring_tac Integral_domain DiscrR ZArith Lia NsatzTactic Rbase Rfunctions RealField