Some lemmas about commutative squares.

I thought these would be used in more places, but I only found one.
I have no objection to combining `isequiv_homotopic` and `cancelR_isequiv` into a named lemma.  I think `(is?)equiv_compose` should be picked up automatically when trying to solve a problem of the form `IsEquiv (_ o _)`, and thus should not need to be combined with `isequiv_homotopic` and `cancelR_isequiv`.