proposition: Lemma mule_neq0 x y : x != 0 -> y != 0 -> x * y != 0.
proof: Proof. move: x y => [x||] [y||] x0 y0 //; rewrite /mule/= ?(lt0y,mulf_neq0)//; try by (rewrite (negbTE x0); case: ifPn) || by (rewrite (negbTE y0); case: ifPn). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed