proposition: Lemma Zmax_gt_compat : forall x y x' y', x > x' -> y > y' -> Z.max x y > Z.max x' y'.
proof: Proof. intros. destruct (Z_ge_dec x y); destruct (Z_ge_dec x' y'); do 2 first [ rewrite Zmax_r; [idtac | lia] | rewrite Zmax_l; [idtac | lia] | idtac ]; lia. Qed.
imports: CoLoR(LogicUtil) Coq(Lia) CoLoR(RelUtil) Coq(Zwf Wellfounded) CoLoR(SN)