proposition: Lemma nat_of_add_pos p q : (p + q)%positive = p + q :> nat.
proof: Proof. apply: @fst _ (Pplus_carry p q = (p + q).+1 :> nat) _. elim: p q => [p IHp|p IHp|] [q|q|] //=; rewrite !natTrecE //; by rewrite ?IHp ?nat_of_succ_pos ?(doubleS, doubleD, addn1, addnS). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring