proposition: Lemma binary_chain_length : forall p, (chain_length (binary_chain p) <= 2 * clog2 p)%nat.
proof: Proof. intro p; unfold binary_chain, chain_length. apply bin_pow_scheme_length1. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)