proposition: Lemma Zle_to_Zmax : forall n m, m <= n -> Z.max n m = n.
proof: Proof. intros n n'; unfold Z.max. intros Hle; cut (n >= n'). unfold Z.ge. case_eq (n ?= n'); intros Heq H; try (elim H; auto; fail). rewrite Zcompare_Eq_eq with (1:=Heq); auto. auto. lia. Qed.
imports: ZArith List Lia