proposition: Lemma BigQ_red_den_nonzero q : match BigQ.red q with BigQ.Qz _ => True | BigQ.Qq _ d => (BigN.to_Z d) <> Z0 end.
proof: Proof. case: q => [//|n d] /=. rewrite /BigQ.norm. rewrite BigN.spec_compare. case: Z.compare_spec => [| |//] Hgcd. { rewrite /BigQ.check_int BigN.spec_compare. case Z.compare_spec => [//| |//] Hd. apply: BigNumPrelude.Zlt0_not_eq. move: Hd; exact: Z.lt_trans. } rewrite /BigQ.check_int BigN.spec_compare. case Z.compare_spec => [//| |//] Hd. apply: BigNumPrelude.Zlt0_not_eq. move: Hd; exact: Z.lt_trans. Qed.
imports: ZArith QArith Lia Bignums(BigQ) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat order) mathcomp(ssralg ssrnum ssrint rat div intdiv) CoqEAL.refinements(hrel refinements param binint)