fact: Fixpoint normal_seq (s : seq R) := if s is a :: l1 then if l1 is b :: l2 then if l2 is c :: l3 then (normal_seq l1) && ((0 == a) || ((a * c <= b^+2) && (0 < a) && (0 < b))) else (0 <= a) && (0 < b) else 0 < a else false.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)