proposition: Lemma mulNR x y : - x * y == - (x * y).
proof: Proof. elim/opp_ind: x => [x | x le0x]; first by rewrite oppK => ->; rewrite oppK. rewrite /mul amulN; case: ifR_cases => le0nx ->; case: ifR_cases => gt0y ->; rewrite ?oppK // (gec0N_eq0 le0x) ?amul0 ?opp0 // ?le0nx -?gt0y // => gt0nx. by case: gt0y; split=> // gt0y; case: le0nx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)