proposition: Lemma elim_lt_Zmax_l : forall x y z, x < y -> x < Z.max y z.
proof: Proof. intros. eapply Z.lt_le_trans. eexact H. apply Z.le_max_l. Qed.
imports: CoLoR(LogicUtil) Coq(Lia) CoLoR(RelUtil) Coq(Zwf Wellfounded) CoLoR(SN)