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.