proposition: Theorem Zfast_div_eucl_correct : forall a b : Z, Zfast_div_eucl a b = Z.div_eucl a b.
proof: Proof. unfold Zfast_div_eucl. intros [|a|a] [|b|b] ; try rewrite Zpos_div_eucl_aux_correct ; easy. Qed.
imports: Coq(ZArith Lia Zquot)