proposition: Lemma graph_relation_compose {k} x y (g g' : graph k) z : graph_relation g x z -> graph_relation g' z y -> graph_relation (g ⋅ g') x y.
proof: Proof. intros gzx g'zy. rewrite -> graph_relation_spec in gzx, g'zy |- *. intros f. specialize (gzx f). simp graph_compose. destruct (g f) as [[[] d]|]; simpl. specialize (g'zy d); destruct (g' d) as [[[] d']|]; simp graph_compose; simpl; lia. specialize (g'zy d). destruct (g' d) as [[[] d']|]; simpl in *. lia. lia. lia. lia. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect