proposition: Lemma Req_EM_var : forall r1 r2 : R, {r1 = r2} + {r1 <> r2}.
proof: Proof. intros; elim (total_order_T r1 r2); intros. elim a; intro. right; red in |- *; intro; rewrite H in a0; elim (Rlt_irrefl r2 a0). left; assumption. right; red in |- *; intro. rewrite H in b; elim (Rlt_irrefl r2 b). Qed.
imports: Reals ails_def trajectory_const