proposition: Lemma MinDistance_lb_pos : (0 < MinDistance_lb)%R.
proof: Proof. Proof with trivial. apply Rlt_trans with (V + ConflictRange)%R... unfold V, ConflictRange in |- *; simpl in |- *; prove_sup... apply MinDistance_lb_majoration... Qed.
imports: Reals trajectory_const rrho trajectory_def