proposition: Lemma ge_A1_not_minusInf : forall a, a >>= A1 -> a <> MinusInf.
proof: Proof. intros. destruct a. discr. destruct H. contr. discr. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)