proposition: Lemma HlrC : l%:C != r%:C.
proof: Proof. by rewrite -!complexr0 eq_complex /= negb_and lt_eqF. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)