proposition: Lemma compose_strong_axioms : forall a b : E, composable a b -> strong_axioms (compose a b).
proof: Proof. ir. unfold strong_axioms in |- *. xe. unfold axioms in |- *. rewrite source_compose. rewrite target_compose. unfold property in |- *. unfold Transformation.axioms in |- *. ir. rewrite ev_compose. unfold composable in H. xe. unfold axioms in H. unfold property in H. unfold Transformation.axioms in H. ap H. unfold axioms in H1. unfold property in H1. unfold Transformation.axioms in H1. rewrite H2. ap H1. am. am. unfold compose in |- *. ap create_like. Qed.
imports: Arith functions