proposition: Lemma axp_scheme_length1 : forall p, (computation_length tt (axp_scheme p tt tt ) <= 2 * clog2 p)%nat.
proof: Proof. induction p; cbn. lia. - destruct p. + lia. + lia. + simpl in IHp; simpl; lia. - lia. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)