proposition: Lemma Zmult_strong_ext_l' : forall z : Z, StrongExtensionality (z *.).
proof: Proof. red;apply (Z_ind3 (fun _ _ _ => _ -> _)). intros [zp zn] [xp xn] [yp yn];rewrite !Zapart_def;unfold PairT.Tapart;simpl. intros E1. refine (merely_destruct (strong_binary_extensionality (+) (zp * (xp + yn)) (zn * (yp + xn)) (zp * (yp + xn)) (zn * (xp + yn)) _) _). - assert (Hrw : zp * (xp + yn) + zn * (yp + xn) = zp * xp + zn * xn + (zp * yn + zn * yp)) by ring_with_nat;rewrite Hrw;clear Hrw. assert (Hrw : zp * (yp + xn) + zn * (xp + yn) = zp * yp + zn * yn + (zp * xn + zn * xp)) by ring_with_nat;rewrite Hrw;exact E1. - intros [E2|E2]. + apply (strong_extensionality (zp *.)). trivial. + apply symmetry;apply (strong_extensionality (zn *.)). trivial. Qed.
imports: HoTT.HIT.quotient HoTT.TruncType HoTT.Basics.Trunc HoTT.Classes.implementations.peano_naturals HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.interfaces.integers HoTT.Classes.theory.rings HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.orders.sum HoTT.Classes.orders.rings HoTT.Classes.tactics.ring_tac HoTT.Classes.theory.naturals