proposition: Lemma eq_plus_eq_is_eq : forall x y z t : R, x = y -> z = t -> (x + z)%R = (y + t)%R.
proof: Proof. intros; rewrite H; rewrite H0; reflexivity. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho