proposition: Lemma BZprodDr n m p: intp n -> intp m -> intp p -> n *z ( m +z p) = (n *z m) +z (n *z p).
proof: Proof. move: n m p. have Qa:forall n m p, inc n BZps -> inc m BZp -> inc p BZp -> n *z ( m +z p) = (n *z m) +z (n *z p). move => n m p pa pb pc. move: (BZps_sBZp pa) => pa'. move: (BZ_valN (BZp_sBZ pa'))(BZ_valN (BZp_sBZ pb))(BZ_valN (BZp_sBZ pc)). move => qa qb qc. move: (BZ_of_natp_i (NS_prod qa qb)) => qe. move: (BZ_of_natp_i (NS_prod qa qc)) => qf. rewrite (BZprod_pp pa' pb)(BZprod_pp pa' pc) (BZprod_pp pa' (ZpS_sum pb pc)). rewrite (BZsum_pp pb pc) (BZsum_pp qe qf) !BZ_of_nat_val. by rewrite cprodDr. have Qb:forall n m p, inc n BZps -> inc m BZp -> inc p BZ -> n *z ( m +z p) = (n *z m) +z (n *z p). move => n m p pa pb; case /BZ_i0P; last by apply: Qa. move => pc; move: (BZps_sBZp pa) => pa'. move: (BZ_valN (BZp_sBZ pa'))(BZ_valN (BZp_sBZ pb))(BZ_valN (BZms_sBZ pc)). move => qa qb qc. move: (BZps_valnz pa) => pa''. have nzp:P n *c P p <> \0c by move:(BZms_hi_pr pc) => [s1 _];apply: cprod2_nz. move: (BZ_of_natp_i (NS_prod qa qb)) => qe. move: (BZm_of_natms_i (NS_prod qa qc) nzp) => qf. rewrite(BZsum_pm pb pc)(BZprod_pp pa' pb)(BZprod_pm pa' pc) (BZsum_pm qe qf). rewrite BZm_of_nat_val BZ_of_nat_val. case: (cleT_el (CS_nat qc) (CS_nat qb)) => le1. have le2: (P n *c P p <=c P n *c P m) by apply: cprod_Mlele; fprops. Ytac0; Ytac0; rewrite (BZprod_pp pa' (BZ_of_natp_i (NS_diff _ qb))). by rewrite BZ_of_nat_val (cprodBl qa qb qc). have le1':= cltNge le1. have le2': ~(P n *c P p <=c P n *c P m). by move => bad; move: (cprod_le2l qa qc qb pa'' bad). move: (NS_diff (P m) qc) => dB. Ytac0; Ytac0;rewrite (BZprod_pm pa' (BZm_of_natms_i dB (cdiff_nz le1))). by rewrite BZm_of_nat_val (cprodBl qa qc qb). have Qc:forall n m p, inc n BZps -> inc m BZ -> inc p BZ -> n *z ( m +z p) = (n *z m) +z (n *z p). move => n m p pa pb pc. case /BZ_i0P: pb => mn; last by apply: Qb. move: (BZms_sBZ mn) (BZps_sBZ pa) => mz nz. move: (Qb _ _ _ pa (BZps_sBZp(BZopp_negative1 mn)) (ZSo pc)). move: (ZSs mz pc) (ZSp nz mz) (ZSp nz pc) => sz sa sb. rewrite - (BZoppD mz pc). rewrite - (BZopp_prod_r nz sz) - (BZopp_prod_r nz mz) - (BZopp_prod_r nz pc). by rewrite - (BZoppD sa sb);apply:BZopp_inj; [ apply: ZSp | apply: ZSs]. have Qd: (forall x y, intp x -> intp y -> (BZopp y) *z x = BZopp (y *z x)). by move => x y xz yz; rewrite (BZopp_prod_r yz xz) (BZprod_opp_comm yz xz). move => n m p. case /BZ_i1P ; first by move => -> _ _; rewrite !BZprod_0l (BZsum_0r ZS0). by apply: Qc. move => nz' mz pz; move: (BZopp_negative1 nz') (BZms_sBZ nz') => nz'' nz. move: (BZps_sBZ nz'') => oz. rewrite - (BZopp_K nz). rewrite (Qd _ _ (ZSs mz pz) oz) (Qd _ _ mz oz) (Qd _ _ pz oz). by rewrite (Qc _ _ _ nz'' mz pz) BZoppD //; apply:ZSp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)