proposition: Lemma Eq_mulA a b c: (a \times (b \times c)) \Eq ((a \times b) \times c).
proof: Proof. pose g z := J (J (P z) (P (Q z))) (Q (Q z)). exists (Lf g (a \times (b \times c)) ((a \times b) \times c)); split; aww. apply: lf_bijective. + move=> d /setX_P [pa pb] /setX_P [pc pd pe]. apply:setXp_i => //; apply:setXp_i => //. + move=> u v /setX_P [pu Pu] /setX_P [pQu PQu QQu] /setX_P [pv Pv] /setX_P [pQv PQv QQv] eq. move:(pr1_def eq)(pr2_def eq)=> eq1 eq2. move:(pr1_def eq1)(pr2_def eq1)=> eq3 eq4. apply: pair_exten=>//; apply: pair_exten =>//. move => y /setX_P [py] /setX_P [pPy PP QP] Qc. exists (J (P (P y)) (J (Q (P y)) (Q y))) => //. apply:setXp_i => //; apply:setXp_i => //. by rewrite /g !(pr1_pair,pr2_pair) pPy py. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)