proposition: Lemma inv_unique: forall x y y', x*y == 1 -> y'*x == 1 -> y==y'.
proof: Proof. intros x y y' Hxy Hy'x. aac_instances <- Hy'x [dot]. aac_rewrite <- Hy'x at 1 [dot]. aac_rewrite Hxy. aac_reflexivity. Qed.
imports: AAC_tactics(AAC)