proposition: Lemma eqnP : Equality.axiom eqn.
proof: Proof. move=> n m; apply: (iffP idP) => [|<-]; last by elim n. by elim: n m => [|n IHn] [|m] //= /IHn->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring