proposition: Lemma diveucl_spec x y : let (q,r) := diveucl x y in (φ q , φ r ) = Z.div_eucl φ x φ y .
proof: Proof. rewrite diveucl_def_spec; unfold diveucl_def; rewrite div_spec, mod_spec; unfold Z.div, Z.modulo. destruct (Z.div_eucl φ x φ y ); trivial. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63