proposition: Lemma Zmax_l : forall x y, x >= y -> Z.max x y = x.
proof: Proof. intros. unfold Z.max. destruct (Dcompare_inf (x ?= y)) as [[xy | xy] | xy]; rewrite xy; try refl. assert (x < y). hyp. lia. Qed.
imports: CoLoR(LogicUtil) Coq(Lia) CoLoR(RelUtil) Coq(Zwf Wellfounded) CoLoR(SN)