proposition: Lemma binary_generator_correct : correct_generator binary_chain.
proof: Proof. red;unfold chain_correct; intros; unfold binary_chain, chain_apply; split;[auto with chains| intros; apply binary_correct]. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)