proposition: Lemma distance_sym : forall s1 s2 : State, distance s1 s2 = distance s2 s1.
proof: Proof. Proof with trivial. intros; unfold distance in |- *; rewrite (Rsqr_neg (xt s2 - xt s1)); rewrite (Rsqr_neg (yt s2 - yt s1)); repeat rewrite Ropp_minus_distr... Qed.
imports: Reals trajectory_const constants ails_def tau Omega