proposition: Lemma semi_invert_left A B C (x : X B A) (x' : X A B) (a b: X A C) : x'*x == 1 -> x*a == x*b -> a == b.
proof: Proof. intros. rewrite <- (dot_neutral_left a). rewrite <- (dot_neutral_left 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)