proposition: Lemma associativity : forall a b c : E, composable a b -> composable b c -> compose (compose a b) c = compose a (compose b c).
proof: Proof. ir. ap extens. ap compose_strong_axioms. unfold composable in |- *. xe. ap compose_axioms; au. unfold composable in H0; xe. rewrite source_compose. unfold composable in H0; xe. ap compose_strong_axioms. unfold composable in |- *; xe. unfold composable in H; xe. ap compose_axioms. am. rewrite target_compose. unfold composable in H; xe. repeat rewrite source_compose. tv. repeat rewrite target_compose; tv. ir. repeat rewrite ev_compose. tv. repeat rewrite source_compose in H1. am. rewrite source_compose in H2. am. repeat rewrite source_compose in H1. unfold composable in H0. xe. rewrite H4. ap H3. am. repeat rewrite source_compose in H1. am. Qed.
imports: Arith functions