proposition: Lemma not_minusInf_ge_A1 : forall a, a <> MinusInf -> a >>= A1.
proof: Proof. intros. destruct a. destruct n. right. refl. left. simpl. lia. tauto. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)