fact: Fixpoint alternate l := if l is a::tl then if a < 0 then alternate_1 tl else if a == 0 then alternate tl else false else false.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol