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