proposition: Lemma allrel_rconsl (r : T -> S -> bool) x xs ys : allrel r (rcons xs x) ys = allrel r xs ys && all (r x) ys.
proof: Proof. by rewrite -cats1 allrel_catl allrel1l. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)