proposition: Lemma infix_rconsl s1 s2 y : infix s1 (rcons s2 y) = suffix s1 (rcons s2 y) || infix s1 s2.
proof: Proof. rewrite -infix_rev rev_rcons infix_consl. by rewrite -rev_rcons prefix_rev infix_rev. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)