proposition: Lemma hcompose_other : forall a b, hcomposable a b -> hcompose a b = hcompose1 a b.
proof: Proof. ir. cp H; uh H; ee. assert (lem1: axioms (hcompose a b)). ap hcompose_axioms; am. assert (lem2 : axioms (hcompose1 a b)). ap hcompose1_axioms; am. ap axioms_extensionality. app hcompose_axioms. app hcompose1_axioms. rw source_hcompose. uf hcompose1. rw source_vcompose. rw source_htrans_right. tv. rw target_hcompose. uf hcompose1. rw target_vcompose. rww target_htrans_left. ir. rwi osource_hcompose H3. rw ntrans_hcompose. uf hcompose1. rw ntrans_vcompose. rw otarget_htrans_left. rw ntrans_htrans_left. rw ntrans_htrans_right. assert (target (target a) = otarget a). tv. rw H4. ap hcomposable_commutativity. am. am. am. am. rw osource_htrans_right. am. am. am. Qed.
imports: Arith functor