fact: Fixpoint neq_elim_aux (lt_l neq_l : seq (term R)) := match neq_l with [::] => [:: lt_l] |neq1 :: neq_l' => let res := neq_elim_aux lt_l neq_l' in let as_pos := map (fun x => neq1 :: x) res in let as_neg := map (fun x => Opp neq1 :: x) res in as_pos ++ as_neg end.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div choice fintype) mathcomp(bigop order ssralg finset fingroup zmodp) mathcomp(poly ssrnum)