proposition: Lemma TypeSpeed_pos : forall h : TypeSpeed, (0 < h)%R.
proof: Proof. intro; assert (H := v_cond1 h). apply Rlt_le_trans with MinSpeed. unfold MinSpeed in |- *; prove_sup. assumption. Qed.
imports: Reals trajectory_const