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