proposition: Lemma bin_of_nat_nat_of_pos_not_0 : forall i, bin_of_nat (nat_of_pos i) <> 0%num.
proof: Proof. elim=> // a Ha /=. rewrite NatTrec.doubleE. contradict Ha. by destruct (nat_of_pos a). Qed.
imports: mathcomp(all_ssreflect fingroup perm)