fact: Definition gpd_moveL_Mh {A : Type} `{Is1Gpd A} {x y z : A} {p : y $-> z} {q : x $-> y} {r : x $-> z} (s : p^$ $o r $== q) : r $== p $o q := ((gpd_h_Vh _ _)^$ $@ (p $@L s)).
imports: Basics.Overture Basics.Tactics