proposition: Lemma mulN1e x : - 1%E * x = - x.
proof: Proof. rewrite -EFinN /mule/=; case: x => [x||]; do ?[by rewrite mulN1r|by rewrite eqe oppr_eq0 oner_eq0 lte_fin ltr0N1]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed