Commit 7b2226a8 by Guillaume Melquiond

Remove useless hypotheses from Max_sym and Min_sym.

From Max_is_some and Max_is_ge, one can prove that ge is a total relation.
So the consequents hold even if "ge x y" does not (since "ge y x" then
holds by totality).
parent dfda5336
 ... ... @@ -73,16 +73,14 @@ exact Zmin_r. Qed. (* Why3 goal *) Lemma Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> Lemma Max_sym : forall (x:Z) (y:Z), ((ZArith.BinInt.Z.max x y) = (ZArith.BinInt.Z.max y x)). intros x y _. apply Zmax_comm. exact Zmax_comm. Qed. (* Why3 goal *) Lemma Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> Lemma Min_sym : forall (x:Z) (y:Z), ((ZArith.BinInt.Z.min x y) = (ZArith.BinInt.Z.min y x)). intros x y _. apply Zmin_comm. exact Zmin_comm. Qed.
 ... ... @@ -42,8 +42,8 @@ theory MinMax axiom Min_x : forall x y:t. ge y x -> min x y = x axiom Min_y : forall x y:t. ge x y -> min x y = y lemma Max_sym: forall x y:t. ge x y -> max x y = max y x lemma Min_sym: forall x y:t. ge x y -> min x y = min y x lemma Max_sym: forall x y:t. max x y = max y x lemma Min_sym: forall x y:t. min x y = min y x (*** function min (x y : t) : t ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!