proposition: Lemma part_function_minus_strext : forall x y (Hx : Conj P Q x) (Hy : Conj P Q y), F x (Prj1 Hx) [-] F' x (Prj2 Hx) [#] F y (Prj1 Hy) [-] F' y (Prj2 Hy) -> x [#] y.
proof: Proof. intros x y Hx Hy H. cut (F x (Prj1 Hx) [#] F y (Prj1 Hy) or F' x (Prj2 Hx) [#] F' y (Prj2 Hy)). intro H0. elim H0; intro H1; exact (pfstrx _ _ _ _ _ _ H1). apply cg_minus_strext; auto. Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CMonoids