[isabelle] which library should be imported in order to prove these



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  		 	   		  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.