proposition: Fact pos_of_natE n m : pos_of_nat n m = Pos.of_succ_nat (n * 2 - m).
proof: Proof. elim: n m => // n IHn [|[|m]] /=; rewrite IHn; lia. Qed.
imports: Coq(ZArith ZifyClasses ZifyInst ZifyBool) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop finset prime) mathcomp(order binomial)