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