proposition: Lemma BinPos_nat_of_P_nat_of_pos : forall i, BinPos.nat_of_P i = nat_of_pos i.
proof: Proof. elim=> // i /= Hi. - by rewrite Pnat.nat_of_P_xI NatTrec.doubleE Hi multE mul2n. - by rewrite Pnat.nat_of_P_xO NatTrec.doubleE Hi multE mul2n. Qed.
imports: mathcomp(all_ssreflect fingroup perm)