proposition: Lemma eq_binP : Equality.axiom N.eqb.
proof: Proof. move=> p q; apply: (iffP idP) => [|<-]; last by case: p => //; elim. by case: q; case: p => //; elim=> [p IHp|p IHp|] [q|q|] //= /IHp [->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring