proposition: Theorem MaxEq : forall (p q : float) (r : R), isMax r p -> isMax r q -> p = q :>R.
proof: Proof. intros p q r H' H'0; apply Rle_antisym. elim H'; intros H'1 H'2; elim H'2; intros H'3 H'4; apply H'4; clear H'2 H'; auto. case H'0; auto. apply isMax_inv1 with (1 := H'0); auto. elim H'0; intros H'1 H'2; elim H'2; intros H'3 H'4; apply H'4; clear H'2 H'0; auto. case H'; auto. apply isMax_inv1 with (1 := H'); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz