proposition: Lemma pow_eq_0_iff : forall a b, a^b == 0 <-> b~=0 /\ a==0.
proof: Proof. intros a b. split. - rewrite pow_eq_0_iff. intros [H |[H H']]. + generalize (le_0_l b); order. + split; order. - intros (Hb,Ha). rewrite Ha. now apply pow_0_l'. Qed.
imports: Bool NAxioms NSub NParity NZPow