proposition: Lemma max_suffix_max l1 l2 k : k `suffix_of` l1 → k `suffix_of` l2 → k `suffix_of` (max_suffix l1 l2).2.
proof: Proof. generalize (max_prefix_max (reverse l1) (reverse l2)). rewrite !suffix_prefix_reverse. unfold max_suffix. destruct (max_prefix (reverse l1) (reverse l2)) as ((?&?)&?); simpl. rewrite reverse_involutive. auto. Qed.
imports: stdpp(options)