proposition: Lemma route_equiv_equivb : forall r r', route_equiv r r' <-> route_eqb r r' = true.
proof: Proof. intros r r' ; rewrite route_equiv_Origin; unfold route_eqb;rewrite Point_eqb_correct;tauto. Qed.
imports: List ZArith Bool Relations Setoid Morphisms RelationClasses EMonoid Lia