proposition: Lemma Npow2_not_zero: forall n, Npow2 n <> 0%N.
proof: Proof. induction n; simpl; intros; [discriminate|]. destruct (Npow2 n); auto. discriminate. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Bool.Bool Coq.Arith.Arith Coq.micromega.Lia Coq.NArith.NArith Coq.ZArith.ZArith bbv.N_Z_nat_conversions bbv.Nomega