fact: Fixpoint pos_of_nat n0 m0 := match n0, m0 with | n.+1, m.+2 => pos_of_nat n m | n.+1, 1 => xO (pos_of_nat n n) | n.+1, 0 => xI (pos_of_nat n n) | 0, _ => xH end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring