proposition: Lemma nat_of_pos_not_0 : forall p, nat_of_pos p <> O.
proof: Proof. elim => // p H. contradict H. rewrite /= NatTrec.doubleE in H. apply/eqP; rewrite -double_eq0; by apply/eqP. Qed.
imports: mathcomp(all_ssreflect fingroup perm)