proposition: Lemma nat_of_pos_inj : forall i j, nat_of_pos i = nat_of_pos j -> i = j.
proof: Proof. elim=> [i Hi [] | i Hi [] | j /=]. - move=> j /= [] /eqP. by rewrite !NatTrec.doubleE -!muln2 eqn_mul2r /= => /eqP/Hi ->. - move=> j /=. rewrite !NatTrec.doubleE => Hj. have absurd : odd ((nat_of_pos j).*2) by rewrite -Hj /= odd_double. by rewrite odd_double in absurd. - rewrite /= NatTrec.doubleE. case => Habsurd. exfalso. move: (@nat_of_pos_not_0 i). by destruct (nat_of_pos i). - move=> j /=. rewrite !NatTrec.doubleE => Hj. have absurd : odd ((nat_of_pos i).*2) by rewrite Hj /= odd_double. by rewrite odd_double in absurd. - move=> j /= /eqP. by rewrite !NatTrec.doubleE -!muln2 eqn_mul2r /= => /eqP/Hi ->. - rewrite /= NatTrec.doubleE => absurd. exfalso. move: (@nat_of_pos_not_0 i). by destruct (nat_of_pos i). destruct j => //=; rewrite NatTrec.doubleE => absurd ; exfalso ; move: (@nat_of_pos_not_0 j) => H' ; by destruct (nat_of_pos j). Qed.
imports: mathcomp(all_ssreflect fingroup perm)