proposition: Theorem ZmaxSym : forall z1 z2 : Z, Zmax z1 z2 = Zmax z2 z1.
proof: Proof. intros z1 z2; unfold Zmax in |- *; CaseEq (z1 ?= z2)%Z; CaseEq (z2 ?= z1)%Z; intros H1 H2; try case (Z.compare_eq _ _ H1); auto; try case (Z.compare_eq _ _ H2); auto; contradict H1. case (Zcompare.Zcompare_Gt_Lt_antisym z2 z1); auto. intros H' H'0; rewrite H'0; auto; red in |- *; intros; discriminate. case (Zcompare.Zcompare_Gt_Lt_antisym z1 z2); auto. intros H'; rewrite H'; auto; intros; red in |- *; intros; discriminate. Qed.
imports: Reals ZArith List PeanoNat Psatz