proposition: Theorem max_l : forall n m, m <= n -> Z.max n m == n.
proof: Proof. unfold Z.max, Z.le, Z.eq; simpl; intros (n1,n2) (m1,m2) H; simpl in *. rewrite max_l by assumption. now rewrite <- add_assoc, (add_comm m2). Qed.
imports: NSub ZAxioms Ring