proposition: Lemma Uinv_max_min : forall x y, [1-](max x y)==min ([1-]x) ([1-]y).
proof: Proof. intros; apply (Ule_total x y); intros; auto. rewrite min_eq_left; auto; rewrite max_eq_left; auto. rewrite min_eq_right; auto; rewrite max_eq_right; auto. Qed.
imports: ALEA(Utheory)