proposition: Lemma ntrans_htrans_right : forall f a x, ob (source f) x -> ntrans (htrans_right a f) x = ntrans a (fob f x).
proof: Proof. ir. uf htrans_right. rw ntrans_create. tv. rw source_fcompose. lu. Qed.
imports: Arith functor