proposition: Lemma max_suffix_snd l1 l2 : l2 = (max_suffix l1 l2).1.2 ++ (max_suffix l1 l2).2.
proof: Proof. rewrite <-(reverse_involutive l2) at 1. rewrite (max_prefix_snd (reverse l1) (reverse l2)). unfold max_suffix. destruct (max_prefix (reverse l1) (reverse l2)) as ((?&?)&?); simpl. by rewrite reverse_app. Qed.
imports: stdpp(options)