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