proposition: Lemma bin_pow_scheme_length1 : forall p, (computation_length tt (bin_pow_scheme p tt ) <= 2 * clog2 p)%nat.
proof: Proof. induction p; cbn. generalize (axp_scheme_length1 p); intro H; lia. destruct p; try lia. cbn. lia. lia. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)