proposition: Lemma ge_bool_cases : forall n m, (if ge_bool n m then n >= m else n < m)%nat.
proof: Proof. intros n; induction n as [|n IHn]; intros m; destruct m as [|m]; simpl; auto with arith. specialize (IHn m). destruct (ge_bool); auto with arith. Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl