proposition: Lemma ZtoRM x y : ZtoR (x * y) = ZtoR x * ZtoR y.
proof: Proof. rewrite /ZtoR. case: ifP => [/Z.ltb_lt lt0 | /Z.ltb_ge ge0]. case: ifP => [/Z.ltb_lt xlt0 | /Z.ltb_ge xge0]. case: ifP => [/Z.ltb_lt ylt0 | /Z.ltb_ge yge0]. suff : Z.lt 0 (x * y) by lia. by apply Z.mul_neg_neg. rewrite !mulNr mulr_natl. rewrite -mulrnA. rewrite !Zabs2Nat.abs_nat_spec !Z.abs_opp Z.abs_mul. rewrite Z2Nat.inj_mul; auto with zarith. by rewrite multE mulnC. case: ifP => [/Z.ltb_lt ylt0 | /Z.ltb_ge yge0]. rewrite mulr_natl. rewrite mulNrn -mulrnA. rewrite !Zabs2Nat.abs_nat_spec !Z.abs_opp Z.abs_mul. rewrite Z2Nat.inj_mul; auto with zarith. by rewrite multE mulnC. suff : Z.le 0 (x * y) by lia. by apply Z.mul_nonneg_nonneg. case: ifP => [/Z.ltb_lt xlt0 | /Z.ltb_ge xge0]. case: ifP => [/Z.ltb_lt ylt0 | /Z.ltb_ge yge0]. rewrite !mulNr mulr_natl. rewrite mulNrn opprK. rewrite -mulrnA. rewrite !Zabs2Nat.abs_nat_spec !Z.abs_opp Z.abs_mul. rewrite Z2Nat.inj_mul; auto with zarith. by rewrite multE mulnC. have [/Z.ltb_lt ygt0 | /negbTE/Z.ltb_ge yeq0] := boolP (Z.ltb 0 y). suff : Z.lt (x * y) 0 by lia. by apply Z.mul_neg_pos. have ->/= : y = Z0 by lia. by rewrite mulr0 Z.mul_0_r. have [/Z.ltb_lt ygt0 | /negbTE/Z.ltb_ge yeq0] := boolP (Z.ltb 0 x); last first. have -> /= : x =Z0 by lia. by rewrite mul0r. case: ifP => [/Z.ltb_lt ylt0 | /Z.ltb_ge yge0]. suff : Z.lt (x * y) 0 by lia. by apply Z.mul_pos_neg. rewrite mulr_natl. rewrite -mulrnA. rewrite !Zabs2Nat.abs_nat_spec Z.abs_mul. rewrite Z2Nat.inj_mul; auto with zarith. by rewrite multE mulnC. Qed.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)