From: Mandy Martin <tesleft@hotmail.com>
Hi ,
which library should be imported in order to prove these
Lemma GCD(A,B) -> A+BLemma Min(A,B) -> Max(A,B)
where A,B are algebra, i do not know the criteria of A and B, would like to find which cases can make lemma above valid and which case is invalid and can auto prove it or how to prove.
Regards,
Martin
Last updated: Jan 26 2026 at 02:06 UTC