proposition: Theorem spec_div_gt: forall x y, [x] > [y] -> 0 < [y] -> let (q,r) := div_gt x y in [q] = [x] / [y] /\ [r] = [x] mod [y].
proof: Proof. intros x y H1 H2; generalize (spec_div_gt_aux x y H1 H2); case div_gt. intros q r (H3, H4); split. apply (Zdiv_unique [x] [y] [q] [r]); auto. rewrite Z.mul_comm; auto. apply (Zmod_unique [x] [y] [q] [r]); auto. rewrite Z.mul_comm; auto. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen