proposition: Lemma pos_gt_3 : forall p:positive, p <> 1 -> p <> 3 -> exact_log2 p = None -> 3 < p.
proof: Proof. intro p;pattern p; apply positive_4step_ind. - destruct 1;auto. - discriminate. - destruct 2;auto. - split; intros; now compute. Qed.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)