add fixpoint lemmas for plain and absorbing

Open William Mansky requested to merge wmansky/iris:master into master

Added some lemmas about typeclass instances for fixpoints on bi_ofeO (as opposed to least/greatest_fixpoint in the logic).

Merge request reports