Some lemmas about commutative squares.

I thought these would be used in more places, but I only found one.
It seems to me that I frequently want to apply this version, so I thought it would be nice to have it as a named lemma rather than having to reprove it every time by applying `cancelR_isequiv`, `isequiv_homotopic` and `equiv_compose`.