proposition: Lemma pow_inj_l : forall a b c, 0<=a -> 0<=b -> 0<c -> a^c == b^c -> a == b.
proof: Proof. intros a b c Ha Hb Hc EQ. destruct (lt_trichotomy a b) as [LT|[EQ'|GT]]; trivial. - assert (a^c < b^c) by (apply pow_lt_mono_l; try split; trivial). order. - assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial). order. Qed.
imports: NZAxioms NZMulOrder