proposition: Lemma Unth_eq : forall n p, n*/ p == [1-]p -> p == [1/]1+n.
proof: Proof. intros; apply Ole_antisym; apply (Ule_total p ([1/]1+n)); intros; auto. apply Uinv_le_simpl. apply Ole_trans with (n*/[1/]1+n); auto. apply Ole_trans with (n*/p); auto. apply Uinv_le_simpl. apply Ole_trans with (n*/p); auto. apply Ole_trans with (n*/[1/]1+n); auto. Qed.
imports: ALEA(Utheory)