proposition: Theorem Pdiv_correct : forall p q, nat_of_P p = oZ (fst (Pdiv p q)) * nat_of_P q + oZ (snd (Pdiv p q)) /\ oZ (snd (Pdiv p q)) < nat_of_P q.
proof: Proof. intros p q; elim p; simpl in |- *; auto with zarith arith. 3: case q; simpl in |- *; try intros q1; split; auto; unfold nat_of_P in |- *; simpl in |- *; auto with arith. intros p'; simpl in |- *; case (Pdiv p' q); simpl in |- *; intros q1 r1 (H1, H2); split. unfold nat_of_P in |- *; simpl in |- *. rewrite ZL6; rewrite H1. case q1; case r1; simpl in |- *. intros r2 q2. rewrite Z.pos_sub_spec; unfold Pos.compare. CaseEq (Pcompare (xI r2) q Datatypes.Eq); simpl in |- *; auto. intros H3; rewrite <- (Pcompare_Eq_eq _ _ H3); simpl in |- *; unfold nat_of_P in |- *; simpl in |- *. apply f_equal with (f := S); repeat rewrite (fun x y => mult_comm x (S y)); repeat rewrite ZL6; unfold nat_of_P in |- *; simpl in |- *; ring. intros H3; unfold nat_of_P in |- *; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- *; ring. intros H3; case (Pminus_mask_Gt _ _ H3); intros h (H4, (H5, H6)); unfold Pminus in |- *; rewrite H4. apply trans_equal with (nat_of_P q + nat_of_P h + Pmult_nat q2 2 * Pmult_nat q 1); [ rewrite <- nat_of_P_plus_morphism; rewrite H5; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- *; apply f_equal with (f := S) | unfold nat_of_P in |- * ]; ring. intros r2. rewrite Z.pos_sub_spec; unfold Pos.compare. CaseEq (Pcompare 1 q Datatypes.Eq); simpl in |- *; auto. intros H3; rewrite <- (Pcompare_Eq_eq _ _ H3); simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- *; simpl in |- *; apply f_equal with (f := S);ring. intros H3; unfold nat_of_P in |- *; simpl in |- *; repeat rewrite (fun x y => Nat.add_comm x (S y)); simpl in |- *; apply f_equal with (f := S); repeat rewrite ZL6; unfold nat_of_P in |- *; simpl in |- *; ring. intros H3; case (Pminus_mask_Gt _ _ H3); intros h (H4, (H5, H6)); unfold Pminus in |- *; rewrite H4; apply trans_equal with (nat_of_P q + nat_of_P h + Pmult_nat r2 2 * Pmult_nat q 1); [ rewrite <- nat_of_P_plus_morphism; rewrite H5; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- *; apply f_equal with (f := S) | unfold nat_of_P in |- * ]; ring. intros r2. rewrite Z.pos_sub_spec; unfold Pos.compare. CaseEq (Pcompare (xI r2) q Datatypes.Eq); simpl in |- *; auto. intros H3; rewrite <- (Pcompare_Eq_eq _ _ H3); simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- *; apply f_equal with (f := S); ring. intros H3; unfold nat_of_P in |- *; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- *; apply f_equal with (f := S); ring. intros H3; case (Pminus_mask_Gt _ _ H3); intros h (H4, (H5, H6)); unfold Pminus in |- *; rewrite H4; apply trans_equal with (nat_of_P q + nat_of_P h); [ rewrite <- (nat_of_P_plus_morphism q); rewrite H5; unfold nat_of_P in |- *; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- *; apply f_equal with (f := S) | unfold nat_of_P in |- * ]; ring. case q; simpl in |- *; auto. generalize H2; case q1; case r1; simpl in |- *; auto. intros r2 q2. rewrite Z.pos_sub_spec; unfold Pos.compare. CaseEq (Pcompare (xI r2) q Datatypes.Eq); simpl in |- *; auto. intros; apply lt_O_nat_of_P; auto. intros H H0; apply nat_of_P_lt_Lt_compare_morphism; auto. intros H3 H7; case (Pminus_mask_Gt _ _ H3); intros h (H4, (H5, H6)); unfold Pminus in |- *; rewrite H4; apply (proj2 (Nat.add_lt_mono_l _ _ (nat_of_P q))); rewrite <- (nat_of_P_plus_morphism q); rewrite H5; unfold nat_of_P in |- *; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- *; apply Nat.le_lt_trans with (Pmult_nat r2 1 + Pmult_nat q 1); auto with arith. intros r2 HH; case q; simpl in |- *; auto. intros p2; apply nat_of_P_lt_Lt_compare_morphism; easy. intros p2; apply nat_of_P_lt_Lt_compare_morphism; easy. intros r2 HH. rewrite Z.pos_sub_spec; unfold Pos.compare. CaseEq (Pcompare (xI r2) q Datatypes.Eq); simpl in |- *. intros; apply lt_O_nat_of_P; auto. intros H3; apply nat_of_P_lt_Lt_compare_morphism; auto. intros H3; case (Pminus_mask_Gt _ _ H3); intros h (H4, (H5, H6)); unfold Pminus in |- *; rewrite H4; apply (proj2 (Nat.add_lt_mono_l _ _ (nat_of_P q))); rewrite <- (nat_of_P_plus_morphism q); rewrite H5; unfold nat_of_P in |- *; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- *; apply Nat.le_lt_trans with (Pmult_nat r2 1 + Pmult_nat q 1); auto with arith. intros HH; case q; simpl in |- *; auto. intros p2; apply nat_of_P_lt_Lt_compare_morphism; easy. intros p2; apply nat_of_P_lt_Lt_compare_morphism; easy. intros p'; simpl in |- *; case (Pdiv p' q); simpl in |- *; intros q1 r1 (H1, H2); split. unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; rewrite H1. case q1; case r1; simpl in |- *; auto. intros r2 q2. rewrite Z.pos_sub_spec; unfold Pos.compare. CaseEq (Pcompare (xO r2) q Datatypes.Eq); simpl in |- *; auto. intros H3; rewrite <- (Pcompare_Eq_eq _ _ H3); simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- *; ring. intros H3; unfold nat_of_P in |- *; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- *; ring. intros H3; case (Pminus_mask_Gt _ _ H3); intros h (H4, (H5, H6)); unfold Pminus in |- *; rewrite H4; apply trans_equal with (nat_of_P q + nat_of_P h + Pmult_nat q2 2 * Pmult_nat q 1); [ rewrite <- (nat_of_P_plus_morphism q); rewrite H5; unfold nat_of_P in |- *; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- * | unfold nat_of_P in |- * ]; ring. intros H3; unfold nat_of_P in |- *; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- *; ring. intros r2. rewrite Z.pos_sub_spec; unfold Pos.compare. CaseEq (Pcompare (xO r2) q Datatypes.Eq); simpl in |- *; auto. intros H3; rewrite <- (Pcompare_Eq_eq _ _ H3); simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- *; ring. intros H3; unfold nat_of_P in |- *; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- *; ring. intros H3; case (Pminus_mask_Gt _ _ H3); intros h (H4, (H5, H6)); unfold Pminus in |- *; rewrite H4; apply trans_equal with (nat_of_P q + nat_of_P h); [ rewrite <- (nat_of_P_plus_morphism q); rewrite H5; unfold nat_of_P in |- *; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- * | unfold nat_of_P in |- * ]; ring. generalize H2; case q1; case r1; simpl in |- *. intros r2 q2. rewrite Z.pos_sub_spec; unfold Pos.compare. CaseEq (Pcompare (xO r2) q Datatypes.Eq); simpl in |- *; auto. intros; apply lt_O_nat_of_P; auto. intros H H0; apply nat_of_P_lt_Lt_compare_morphism; auto. intros H3 H7; case (Pminus_mask_Gt _ _ H3); intros h (H4, (H5, H6)); unfold Pminus in |- *; rewrite H4; apply (proj2 (Nat.add_lt_mono_l _ _ (nat_of_P q))); rewrite <- (nat_of_P_plus_morphism q); rewrite H5; unfold nat_of_P in |- *; simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- *; apply Nat.lt_trans with (Pmult_nat r2 1 + Pmult_nat q 1); auto with arith. intros; apply lt_O_nat_of_P; auto. intros r2 HH. rewrite Z.pos_sub_spec; unfold Pos.compare. CaseEq (Pcompare (xO r2) q Datatypes.Eq); simpl in |- *. intros; apply lt_O_nat_of_P; auto. intros H3; apply nat_of_P_lt_Lt_compare_morphism; auto. intros H3; case (Pminus_mask_Gt _ _ H3); intros h (H4, (H5, H6)); unfold Pminus in |- *; rewrite H4; apply (proj2 (Nat.add_lt_mono_l _ _ (nat_of_P q))); rewrite <- (nat_of_P_plus_morphism q); rewrite H5; unfold nat_of_P in |- *; simpl in |- *; repeat rewrite ZL6; unfold nat_of_P in |- *; apply Nat.lt_trans with (Pmult_nat r2 1 + Pmult_nat q 1); auto with arith. auto. rewrite ZL6; generalize (Pos2Nat.is_pos q1); auto with zarith arith. rewrite ZL6; generalize (Pos2Nat.is_pos q1); auto with zarith arith. Qed.
imports: Reals ZArith List PeanoNat Psatz