proposition: Lemma optimal_upper_bound: forall p c, optimal p c -> (chain_length c <= 2 * clog2 p)%nat.
proof: Proof. unfold optimal;intros p c H. transitivity (chain_length (binary_chain p)). - apply H; apply binary_generator_correct. - apply binary_chain_length. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)