proposition: Theorem minProp5 : forall a b : rZ, eqRz a b -> min a b = b.
proof: Proof. intros a b; unfold min in |- *; case (rZltDec a b); simpl in |- *; auto with stalmarck. intros H'0 H'1; absurd (eqRz a b); auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)