proposition: Lemma part_function_mult_strext : forall x y (Hx : Conj P Q x) (Hy : Conj P Q y), F x (Prj1 Hx) [*]G x (Prj2 Hx) [#] F y (Prj1 Hy) [*]G y (Prj2 Hy) -> x [#] y.
proof: Proof. intros x y Hx Hy H. elim (bin_op_strext_unfolded _ _ _ _ _ _ H); intro H1; exact (pfstrx _ _ _ _ _ _ H1). Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CSums CoRN.algebra.CAbMonoids Coq.Sorting.Permutation CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms Coq(Lia)