Skip to content

Add big_andM

Michael Sammler requested to merge msammler/big_andM into master

This MR adds big_andM, similar to big_andL. I am not sure which lemmas to add so I just copied the lemmas from big_sepM and commented out the ones that I could not directly prove. Please let me know which lemmas should be ported to big_andM and which should be removed.

Merge request reports