proposition: Lemma ZtoRD (x y : Z) : 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]. rewrite -!mulNrn -mulrnDr; congr (_ *+ _). rewrite Z.opp_add_distr Zabs2Nat.inj_add ?plusE //. rewrite Z.opp_nonneg_nonpos. by apply: Z.lt_le_incl. by apply /Z.opp_nonneg_nonpos/Z.lt_le_incl. rewrite -!mulNrn -[X in _ + X *+ _]opprK. rewrite (mulNrn (-1)). rewrite -mulrnBr; last by apply/leP; lia. rewrite -minusE. rewrite -Zabs2Nat.inj_sub; last by lia. by rewrite Z.opp_add_distr. case: ifP => [/Z.ltb_lt ylt0 | /Z.ltb_ge yge0]. rewrite -!mulNrn -[X in X *+ _ + _]opprK. rewrite (mulNrn (-1)). rewrite addrC -mulrnBr; last by apply/leP; lia. rewrite -minusE. rewrite -Zabs2Nat.inj_sub; last by lia. by rewrite Z.add_comm Z.opp_add_distr. suff : False by []. lia. case: ifP => [/Z.ltb_lt xlt0 | /Z.ltb_ge xge0 ]. case: ifP => [/Z.ltb_lt ylt0 | /Z.ltb_ge yge0]. suff : False by []. lia. rewrite addrC -mulrnBr; last by apply/leP; lia. rewrite -minusE -Zabs2Nat.inj_sub; last by lia. by rewrite Z.sub_opp_r Z.add_comm. case: ifP => [/Z.ltb_lt ylt0 | /Z.ltb_ge yge0]. rewrite -mulrnBr; last by apply/leP; lia. rewrite -minusE -Zabs2Nat.inj_sub; last by lia. by rewrite Z.sub_opp_r Z.add_comm. rewrite -mulrnDr. by rewrite -plusE -Zabs2Nat.inj_add. Qed.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)