proposition: Lemma joinAC (x y z : U) : x \+ y \+ z = x \+ z \+ y.
proof: Proof. Admitted. Lemma joinCA (x y z : U) : x \+ (y \+ z) = y \+ (x \+ z). Proof. Admitted. Lemma validL (x y : U) : valid (x \+ y) -> valid x. Proof. Admitted. Lemma validR (x y : U) : valid (x \+ y) -> valid y. Proof. Admitted. Lemma unitL (x : U) : (@Unit U) \+ x = x. Proof. Admitted. Lemma unitR (x : U) : x \+ (@Unit U) = x. Proof. Admitted. Lemma valid_unit : valid (@Unit U). Proof. Admitted. End PCMLemmas. End Exports. End PCMDef. Export PCMDef.Exports. Module CancelPCM. Record mixin_of (U : pcm) := Mixin { _ : forall a b c: U, valid (a \+ b) -> a \+ b = a \+ c -> b = c }. Structure pack_type : Type := Pack {pcmT : pcm; _ : mixin_of pcmT}. Module Exports. Notation cancel_pcm := pack_type. Notation CancelPCMMixin := Mixin. Notation CancelPCM T m:= (@Pack T m). Coercion pcmT : pack_type >-> pcm. Lemma cancel (U: cancel_pcm) (x y z: U): valid (x \+ y) -> x \+ y = x \+ z -> y = z. Proof. by case: U x y z=>Up [Hc] x y z; apply: Hc. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun)