proposition: Lemma rem_rcons1 a b l: a < b -> rem a (rcons l b) = rcons (rem a l) b.
proof: Proof. move => h; elim:l => /=; first by rewrite gtn_eqF. by move => x l H /=; case:(x==a) => //; rewrite H rcons_cons. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)