proposition: Lemma eqb_eq n m : eqb n m = true <-> n = m.
proof: Proof. revert m. induction n as [|n IHn]; intro m; destruct m; simpl; rewrite ?IHn; split; try easy. - now intros ->. - now injection 1. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass