Zmult_strong_ext_l' : forall z : Z, StrongExtensionality (z *.). 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.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.