proposition: Lemma nat_of_P_minus_morphism p q : Pos.compare_cont Eq p q = Gt -> Pos.to_nat (p - q) = Pos.to_nat p - Pos.to_nat q.
proof: Proof. Proof (fun H => Pos2Nat.inj_sub p q (Pos.gt_lt _ _ H)). Lemma nat_of_P_lt_Lt_compare_morphism p q : Pos.compare_cont Eq p q = Lt -> Pos.to_nat p < Pos.to_nat q. Proof (proj1 (Pos2Nat.inj_lt p q)). Lemma nat_of_P_gt_Gt_compare_morphism p q : Pos.compare_cont Eq p q = Gt -> Pos.to_nat p > Pos.to_nat q. Proof (proj1 (Pos2Nat.inj_gt p q)). Lemma nat_of_P_lt_Lt_compare_complement_morphism p q : Pos.to_nat p < Pos.to_nat q -> Pos.compare_cont Eq p q = Lt. Proof (proj2 (Pos2Nat.inj_lt p q)). Definition nat_of_P_gt_Gt_compare_complement_morphism p q : Pos.to_nat p > Pos.to_nat q -> Pos.compare_cont Eq p q = Gt. Proof (proj2 (Pos2Nat.inj_gt p q)). Section ObsoletePmultNat. Lemma Pmult_nat_mult : forall p n, Pmult_nat p n = Pos.to_nat p * n. Proof. intro p; induction p as [p IHp|p IHp|]; intros n; unfold Pos.to_nat; simpl. - f_equal. rewrite 2 IHp. rewrite <- Nat.mul_assoc. f_equal. simpl. now rewrite Nat.add_0_r. - rewrite 2 IHp. rewrite <- Nat.mul_assoc. f_equal. simpl. now rewrite Nat.add_0_r. - simpl. now rewrite Nat.add_0_r. Qed.
imports: BinPos PeanoNat