proposition: Lemma prefix_rcons a b c : prefix a (rcons b c) = prefix a b || (a == rcons b c).
proof: Proof. rewrite /prefix -cats1 take_cat; case: ifPn => [ab|]. rewrite (_ : _ == b ++ _ = false) ?orbF //; apply/negbTE. apply: contraTN ab => /eqP ->; by rewrite -leqNgt size_cat leq_addr. rewrite -leqNgt leq_eqVlt => /orP[/eqP|] ab. rewrite -ab subnn take0 cats0 take_size (_ : _ == _ ++ _ = false) ?orbF //. apply/negbTE/eqP => /(congr1 size)/eqP. by rewrite size_cat ab -{1}(addn0 (size a)) eqn_add2l. rewrite take_oversize /= ?subn_gt0 // (_ : _ == take _ _ = false) //. apply/negbTE; move: (ab). rewrite ltnNge; apply: contra => /eqP ->; by rewrite size_take ltnNge (ltnW ab). Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext