fact: Fixpoint remove (x : nat) (l : list nat) : list nat := match l with | [] => [] | h::t => if beq_nat h x then t else h :: remove x t end.
imports: QuickChick(QuickChick) List ZArith mathcomp(seq ssreflect ssrbool ssrnat eqtype)