proposition: Lemma arctic_plus_ge_monotone : forall (a b c : A), a >>= c -> Aplus a b >>= c.
proof: Proof. intros. destruct c. destruct a. destruct b. simpl. arctic_ord. apply Z.le_ge. apply elim_Zmax_l. lia. trivial. arctic_ord. apply minusInf_ge_min. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)