proposition: Theorem imp_trans' (P Q R: Prop) : (Q -> R) -> (P -> Q) -> P -> R.
proof: Proof. move=> H1 H2. move: (imp_trans P Q R)=> H. apply: H. done. done. Restart. move: (imp_trans P Q R)=> H H1 H2. apply: H; done. Restart. move=>H1 H2; apply: (imp_trans P Q R)=>//. Qed.
imports: mathcomp(ssreflect)