fact: Fixpoint ge_bool (n m : nat) : bool := match n with | O => match m with | O => true | S _ => false end | S n => match m with | O => true | S m => ge_bool n m end end.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl