proposition: Lemma pos_of_natE m n : pos_of_nat m n = Pos.of_nat (maxn 1 (m.*2.+1 - n)).
proof: Proof. elim: m n => [|m IHm] n; first by rewrite /= double0 (maxn_idPl (leq_subr _ _)). simpl. case: n => [|n]; last case: n => [|n]; last by rewrite IHm. - rewrite subn0 IHm. have->: (m.*2.+1 - m = m.+1)%N. rewrite -addnn subSn; first by rewrite addnK. exact: leq_addr. by rewrite !(maxn_idPr _) // Nat2Pos_xI. - rewrite subn1 IHm. have->: (m.*2.+1 - m = m.+1)%N. rewrite -addnn subSn; first by rewrite addnK. exact: leq_addr. by rewrite !(maxn_idPr _) // Nat2Pos_xO. Qed.
imports: ZArith Lia mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg ssrnum bigop ssrint) CoqEAL(hrel param refinements pos)