proposition: Lemma Q_one_zero: not (Qeq 1%Q 0%Q).
proof: Proof. unfold Qeq. simpl. lia. Qed.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool Algebra_syntax Ncring Ncring_initial Ncring_tac Integral_domain ZArith Lia QArith