proposition: Theorem Pdiv_le: forall p q, Zpos p <= Zpos q * Zpos (Pdiv p q).
proof: Proof. intros p q. unfold Pdiv. assert (H1: Zpos q > 0) by auto with zarith. assert (H1b: Zpos p >= 0) by auto with zarith. generalize (Z_div_ge0 (Zpos p) (Zpos q) H1 H1b). generalize (Z_div_mod_eq_full (Zpos p) (Zpos q)); case Z.div. intros HH _; rewrite HH; rewrite Z.mul_0_r; rewrite Z.mul_1_r; simpl. case (Z_mod_lt (Zpos p) (Zpos q) H1); auto with zarith. intros q1 H2. replace (Zpos p - Zpos q * Zpos q1) with (Zpos p mod Zpos q). 2: pattern (Zpos p) at 2; rewrite H2; auto with zarith. generalize H2 (Z_mod_lt (Zpos p) (Zpos q) H1); clear H2; case Z.modulo. intros HH _; rewrite HH; auto with zarith. intros r1 HH (_,HH1); rewrite HH; rewrite Pos2Z.inj_succ. unfold Z.succ; rewrite Z.mul_add_distr_l; auto with zarith. intros r1 _ (HH,_); case HH; auto. intros q1 HH; rewrite HH. unfold Z.ge; simpl Z.compare; intros HH1; case HH1; auto. Qed.
imports: ZArith Lia Ndigits BigNumPrelude DoubleType DoubleBase CyclicAxioms DoubleCyclic