proposition: Lemma leb_le n m : (n <=? m) = true <-> n <= m.
proof: Proof. revert m. induction n as [|n IHn]; intro m; destruct m; simpl. - now split. - split; trivial. intros; apply Peano.le_0_n. - now split. - rewrite IHn; split. + apply Peano.le_n_S. + apply Peano.le_S_n. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass