proposition: Lemma Zmax_ge_compat : forall x y x' y', x >= x' -> y >= y' -> Z.max x y >= Z.max x' y'.
proof: Proof. intros. destruct (Zmax_irreducible_inf x' y'); rewrite e; unfold ge. rewrite Z.max_comm. apply Z.le_ge. apply elim_Zmax_r. lia. apply Z.le_ge. apply elim_Zmax_r. lia. Qed.
imports: CoLoR(LogicUtil) Coq(Lia) CoLoR(RelUtil) Coq(Zwf Wellfounded) CoLoR(SN)