fact: Fixpoint leb (n m: nat) : bool := match n with | O => match m with | O => true | S m' => true end | S n' => match m with | O => false | S m' => leb n' m' end end.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance