proposition: Theorem Zquot_mod_unique_full a b q r : Remainder a b r -> a = b*q + r -> q = a÷b /\ r = Z.rem a b.
proof: Proof. destruct 1 as [(H,H0)|(H,H0)]; intros. - apply Zdiv_mod_unique with b; auto. + apply Zrem_lt_pos; auto. lia. + rewrite <- H1; apply Z.quot_rem'. - rewrite <- (Z.opp_involutive a). rewrite Zquot_opp_l, Zrem_opp_l. generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Z.rem (-a) b)). generalize (Zrem_lt_pos (-a) b). rewrite <-Z.quot_rem', Z.mul_opp_r, <-Z.opp_add_distr, <-H1. lia. Qed.
imports: Nnat ZArith_base Lia ZArithRing Zdiv Morphisms