proposition: Lemma muleN x y : x * - y = - (x * y).
proof: Proof. move: x y => [x| |] [y| |] //=; rewrite /mule/=; try by rewrite ltry. - by rewrite mulrN. - by rewrite !eqe !lte_fin; case: ltrgtP => //; rewrite oppe0. - by rewrite !eqe !lte_fin; case: ltrgtP => //; rewrite oppe0. - rewrite !eqe oppr_eq0 eq_sym; case: ifP; rewrite ?oppe0// => y0. by rewrite [RHS]fun_if ltNge if_neg EFinN leeNl oppe0 le_eqVlt eqe y0. - rewrite !eqe oppr_eq0 eq_sym; case: ifP; rewrite ?oppe0// => y0. by rewrite [RHS]fun_if ltNge if_neg EFinN leeNl oppe0 le_eqVlt eqe y0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed