proposition: Lemma Uexp_lt_compat : forall p q n, (O<n)%nat->(p<q)->(p^n<q^n).
proof: Proof. induction n; simpl; intros; auto. casetype False; lia. destruct n; auto. apply Umult_lt_compat; auto with arith. Qed.
imports: ALEA(Utheory)