proposition: Lemma semi_invert_right A B C (x : X C B) (x' : X B C) (a b: X A C) : x * x' == 1 -> a*x == b*x -> a == b.
proof: Proof. intros. rewrite <- (dot_neutral_right a). rewrite <- (dot_neutral_right b). rewrite <- H. rewrite 2 dot_assoc. auto with compat. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)