proposition: Lemma cp_min_trans : forall x y z, cp_min x y = x -> cp_min y z = y -> cp_min x z = x.
proof: Proof. intros [x | | ] [y| |]; try (simpl; intros; discriminate); intros [z | | ]; try(simpl; intros; discriminate); simpl; auto. intros H1 H2; injection H1; injection H2; intros H3 H4. rewrite Zle_to_Zmin; auto. apply Z.le_trans with y. rewrite <-H4; auto with zarith. rewrite <- H3; auto with zarith. Qed.
imports: ZArith List Lia