(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Require Import Reals.
Require Import trajectory_const.

Definition rho (h : TypeSpeed) : R := (g * (tan MaxBank / h))%R.
Definition r (h : TypeSpeed) : R := (h / rho h)%R.
Definition rho_ub (h : TypeSpeed) : R := (g * (tan_ub_MaxBank / h))%R.
Definition rho_lb (h : TypeSpeed) : R := (g * (tan_lb_MaxBank / h))%R.

(**********)
Lemma TypeSpeed_pos : forall h : TypeSpeed, (0 < h)%R.
(* Goal: forall h : TypeSpeed, Rlt (IZR Z0) (v h) *)
intro; assert (H := v_cond1 h).
(* Goal: Rlt (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH))))))))) (v h) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
apply Rlt_le_trans with MinSpeed.
(* Goal: Rlt (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH))))))))) MinSpeed *)
(* Goal: Rle MinSpeed (v h) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
unfold MinSpeed in |- *; prove_sup.
(* Goal: Rle MinSpeed (v h) *)
assumption.
Qed.

(**********)
Lemma g_pos : (0 < g)%R.
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
unfold g in |- *; unfold Rdiv in |- *; apply Rmult_lt_reg_l with 10%R.
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO (xI (xO xH))))) *)
(* Goal: Rlt (Rmult (IZR (Zpos (xO (xI (xO xH))))) (Rmult (IZR (Zpos (xO (xI (xO (xO (xO (xO (xI (xO xH)))))))))) (Rinv (IZR (Zpos (xO (xI (xO xH)))))))) (Rmult (IZR (Zpos (xO (xI (xO xH))))) (IZR (Zpos (xI (xO (xO (xO (xO xH)))))))) *)
prove_sup.
rewrite Rmult_0_r; rewrite <- Rmult_comm; rewrite Rmult_assoc;
 rewrite <- Rinv_l_sym; [ prove_sup | discrR ].
Qed.

(**********)
Lemma rho_ub_0 : forall h : TypeSpeed, (rho h < rho_ub h)%R.
intros; unfold rho, rho_ub in |- *; apply Rmult_lt_compat_l;
 [ apply g_pos
 | generalize TypeSpeed_pos; intros; generalize (H h); clear H; intro H;
    generalize (Rinv_0_lt_compat h H); intro H1; generalize tan_MaxBank_ub;
    intro H2;
    generalize (Rmult_lt_compat_l (/ h) (tan MaxBank) tan_ub_MaxBank H1 H2);
    rewrite Rmult_comm; rewrite <- (Rmult_comm tan_ub_MaxBank); 
    intro H3; assumption ].
Qed.

(**********)
Lemma rho_lb_0 : forall h : TypeSpeed, (rho_lb h < rho h)%R.
intros; unfold rho, rho_lb in |- *; apply Rmult_lt_compat_l;
 [ apply g_pos
 | generalize TypeSpeed_pos; intros; generalize (H h); clear H; intro H;
    generalize (Rinv_0_lt_compat h H); intro H1; generalize tan_MaxBank_lb;
    intro H2;
    generalize (Rmult_lt_compat_l (/ h) tan_lb_MaxBank (tan MaxBank) H1 H2);
    rewrite <- (Rmult_comm (tan MaxBank));
    rewrite <- (Rmult_comm tan_lb_MaxBank); intro H3; 
    assumption ].
Qed.

Definition r_ub (h : TypeSpeed) : R := (h / rho_lb h)%R.
Definition r_lb (h : TypeSpeed) : R := (h / rho_ub h)%R.

(**********)
Lemma tan_lb_MaxBank_pos : (0 < tan_lb_MaxBank)%R.
unfold tan_lb_MaxBank in |- *; unfold Rdiv in |- *;
 apply Rmult_lt_reg_l with 10%R.
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO (xI (xO xH))))) *)
(* Goal: Rlt (Rmult (IZR (Zpos (xO (xI (xO xH))))) (Rmult (IZR (Zpos (xO (xI (xO (xO (xO (xO (xI (xO xH)))))))))) (Rinv (IZR (Zpos (xO (xI (xO xH)))))))) (Rmult (IZR (Zpos (xO (xI (xO xH))))) (IZR (Zpos (xI (xO (xO (xO (xO xH)))))))) *)
prove_sup.
rewrite Rmult_0_r; rewrite <- Rmult_comm; rewrite Rmult_assoc;
 rewrite <- Rinv_l_sym; [ prove_sup | discrR ].
Qed.

(**********)
Lemma tan_ub_MaxBank_pos : (0 < tan_ub_MaxBank)%R.
apply Rlt_trans with tan_lb_MaxBank;
 [ apply tan_lb_MaxBank_pos
 | apply Rlt_trans with (tan MaxBank);
    [ apply tan_MaxBank_lb | apply tan_MaxBank_ub ] ].
Qed.

(**********)
Lemma rho_lb_pos : forall h : TypeSpeed, (0 < rho_lb h)%R.
intros; unfold rho_lb in |- *; apply Rmult_lt_0_compat;
 [ apply g_pos
 | replace (tan_lb_MaxBank / h)%R with (tan_lb_MaxBank * / h)%R;
    [ rewrite Rmult_comm; generalize TypeSpeed_pos; intro H; generalize (H h);
       clear H; intro H; generalize (Rinv_0_lt_compat h H); 
       intro H0; apply Rmult_lt_0_compat;
       [ assumption | apply tan_lb_MaxBank_pos ]
    | auto ] ].
Qed.

(**********)
Lemma rho_pos : forall h : TypeSpeed, (0 < rho h)%R.
(* Goal: forall h : TypeSpeed, Rlt (IZR Z0) (rho h) *)
intro; apply Rlt_trans with (rho_lb h); [ apply rho_lb_pos | apply rho_lb_0 ].
Qed.

(**********)
Lemma rho_ub_pos : forall h : TypeSpeed, (0 < rho_ub h)%R.
(* Goal: forall h : TypeSpeed, Rlt (IZR Z0) (rho_ub h) *)
intro; apply Rlt_trans with (rho h); [ apply rho_pos | apply rho_ub_0 ].
Qed.

(**********)
Lemma r_ub_0 : forall h : TypeSpeed, (r h < r_ub h)%R.
intros; unfold r, r_ub in |- *; generalize (rho_lb_0 h); intro H;
 generalize (Rmult_lt_0_compat (rho_lb h) (rho h) (rho_lb_pos h) (rho_pos h));
 intro H0; generalize (Rinv_lt_contravar (rho_lb h) (rho h) H0 H); 
 intro H1;
 generalize (Rmult_lt_compat_l h (/ rho h) (/ rho_lb h) (TypeSpeed_pos h) H1);
(* Goal: Rle MinSpeed (v h) *)
 intro H2; assumption.
Qed.

(**********)
Lemma r_lb_0 : forall h : TypeSpeed, (r_lb h < r h)%R.
intros; unfold r, r_lb in |- *; generalize (rho_ub_0 h); intro H;
 generalize (Rmult_lt_0_compat (rho h) (rho_ub h) (rho_pos h) (rho_ub_pos h));
 intro H0; generalize (Rinv_lt_contravar (rho h) (rho_ub h) H0 H); 
 intro H1;
 generalize (Rmult_lt_compat_l h (/ rho_ub h) (/ rho h) (TypeSpeed_pos h) H1);
(* Goal: Rle MinSpeed (v h) *)
 intro H2; assumption.
Qed.

(**********)
Lemma rho_PI2 : forall h : TypeSpeed, (rho h <= PI / 2)%R.
(* Goal: forall h : TypeSpeed, Rle (rho h) (Rdiv PI (IZR (Zpos (xO xH)))) *)
intro h; unfold rho in |- *; unfold Rdiv in |- *.
(* Goal: Rle (Rmult g (Rmult (tan MaxBank) (Rinv (v h)))) (Rmult PI (Rinv (IZR (Zpos (xO xH))))) *)
cut (g < 33)%R.
(* Goal: forall _ : Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))), Rle (Rmult g (Rmult (tan MaxBank) (Rinv (v h)))) (Rmult PI (Rinv (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
cut (tan MaxBank < 1)%R.
(* Goal: forall (_ : Rlt (tan MaxBank) (IZR (Zpos xH))) (_ : Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH)))))))), Rle (Rmult g (Rmult (tan MaxBank) (Rinv (v h)))) (Rmult PI (Rinv (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
cut (/ h < / 200)%R.
intros; generalize g_pos; intro H2; generalize tan_MaxBank_pos; intro H3;
 generalize (Rinv_0_lt_compat h (TypeSpeed_pos h)); 
 intro H4.
generalize
 (Rmult_le_0_lt_compat g 33 (tan MaxBank) 1 (Rlt_le 0 g H2)
    (Rlt_le 0 (tan MaxBank) H3) H1 H0); intro H5;
 generalize (Rmult_lt_0_compat g (tan MaxBank) H2 H3); 
 intro H6.
(* Goal: Rle (Rmult g (Rmult (tan MaxBank) (Rinv (v h)))) (Rmult PI (Rinv (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rinv (v h)) (Rinv (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH)))))))))) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
rewrite Rmult_1_r in H5.
generalize
 (Rmult_le_0_lt_compat (g * tan MaxBank) 33 (/ h) (/ 200)
    (Rlt_le 0 (g * tan MaxBank) H6) (Rlt_le 0 (/ h) H4) H5 H).
(* Goal: forall _ : Rlt (Rmult (Rmult g (tan MaxBank)) (Rinv (v h))) (Rmult (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) (Rinv (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH))))))))))), Rle (Rmult g (Rmult (tan MaxBank) (Rinv (v h)))) (Rmult PI (Rinv (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rinv (v h)) (Rinv (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH)))))))))) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
intro H7; left.
(* Goal: Rlt (Rmult g (Rmult (tan MaxBank) (Rinv (v h)))) (Rmult PI (Rinv (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rinv (v h)) (Rinv (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH)))))))))) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
apply Rlt_trans with (33 / 200)%R.
(* Goal: Rle MinSpeed (v h) *)
unfold Rdiv in |- *; rewrite <- Rmult_assoc; assumption.
(* Goal: Rlt (Rdiv (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH)))))))))) (Rmult PI (Rinv (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rinv (v h)) (Rinv (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH)))))))))) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
apply Rlt_le_trans with (PI_lb / 2)%R.
(* Goal: Rlt (Rdiv (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH)))))))))) (Rdiv PI_lb (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rdiv PI_lb (IZR (Zpos (xO xH)))) (Rmult PI (Rinv (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rinv (v h)) (Rinv (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH)))))))))) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
apply Rlt_trans with 1%R.
(* Goal: Rlt (Rdiv (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH)))))))))) (IZR (Zpos xH)) *)
(* Goal: Rlt (IZR (Zpos xH)) (Rdiv PI_lb (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rdiv PI_lb (IZR (Zpos (xO xH)))) (Rmult PI (Rinv (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rinv (v h)) (Rinv (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH)))))))))) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
unfold Rdiv in |- *; apply Rmult_lt_reg_l with 200%R.
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO (xI (xO xH))))) *)
(* Goal: Rlt (Rmult (IZR (Zpos (xO (xI (xO xH))))) (Rmult (IZR (Zpos (xO (xI (xO (xO (xO (xO (xI (xO xH)))))))))) (Rinv (IZR (Zpos (xO (xI (xO xH)))))))) (Rmult (IZR (Zpos (xO (xI (xO xH))))) (IZR (Zpos (xI (xO (xO (xO (xO xH)))))))) *)
prove_sup.
rewrite Rmult_1_r; rewrite <- Rmult_comm; rewrite Rmult_assoc;
 rewrite <- Rinv_l_sym; [ prove_sup | discrR ].
(* Goal: Rlt (IZR (Zpos xH)) (Rdiv PI_lb (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rdiv PI_lb (IZR (Zpos (xO xH)))) (Rmult PI (Rinv (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rinv (v h)) (Rinv (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH)))))))))) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
apply Rmult_lt_reg_l with 2%R.
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO (xI (xO xH))))) *)
(* Goal: Rlt (Rmult (IZR (Zpos (xO (xI (xO xH))))) (Rmult (IZR (Zpos (xO (xI (xO (xO (xO (xO (xI (xO xH)))))))))) (Rinv (IZR (Zpos (xO (xI (xO xH)))))))) (Rmult (IZR (Zpos (xO (xI (xO xH))))) (IZR (Zpos (xI (xO (xO (xO (xO xH)))))))) *)
prove_sup.
unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
 rewrite <- Rinv_r_sym.
(* Goal: Rlt (Rmult (IZR (Zpos (xO xH))) (IZR (Zpos xH))) (Rmult (IZR (Zpos xH)) PI_lb) *)
(* Goal: not (@eq R (IZR (Zpos (xO xH))) (IZR Z0)) *)
(* Goal: Rle (Rdiv PI_lb (IZR (Zpos (xO xH)))) (Rmult PI (Rinv (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rinv (v h)) (Rinv (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH)))))))))) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
rewrite Rmult_1_r; rewrite Rmult_1_l; unfold PI_lb in |- *.
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO (xI (xO xH))))) *)
(* Goal: Rlt (Rmult (IZR (Zpos (xO (xI (xO xH))))) (Rmult (IZR (Zpos (xO (xI (xO (xO (xO (xO (xI (xO xH)))))))))) (Rinv (IZR (Zpos (xO (xI (xO xH)))))))) (Rmult (IZR (Zpos (xO (xI (xO xH))))) (IZR (Zpos (xI (xO (xO (xO (xO xH)))))))) *)
prove_sup.
(* Goal: not (@eq R (IZR (Zpos (xO xH))) (IZR Z0)) *)
(* Goal: Rle (Rdiv PI_lb (IZR (Zpos (xO xH)))) (Rmult PI (Rinv (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rinv (v h)) (Rinv (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH)))))))))) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
discrR.
unfold Rdiv in |- *; left; repeat rewrite <- (Rmult_comm (/ 2));
 apply Rmult_lt_compat_l.
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO (xI (xO xH))))) *)
(* Goal: Rlt (Rmult (IZR (Zpos (xO (xI (xO xH))))) (Rmult (IZR (Zpos (xO (xI (xO (xO (xO (xO (xI (xO xH)))))))))) (Rinv (IZR (Zpos (xO (xI (xO xH)))))))) (Rmult (IZR (Zpos (xO (xI (xO xH))))) (IZR (Zpos (xI (xO (xO (xO (xO xH)))))))) *)
apply Rinv_0_lt_compat; prove_sup.
(* Goal: Rle MinSpeed (v h) *)
elim PI_approx; intros; assumption.
(* Goal: Rlt (Rinv (v h)) (Rinv (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH)))))))))) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
apply Rinv_lt_contravar.
(* Goal: Rlt (IZR Z0) (Rmult (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH))))))))) (v h)) *)
(* Goal: Rlt (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH))))))))) (v h) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
apply Rmult_lt_0_compat.
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO (xI (xO xH))))) *)
(* Goal: Rlt (Rmult (IZR (Zpos (xO (xI (xO xH))))) (Rmult (IZR (Zpos (xO (xI (xO (xO (xO (xO (xI (xO xH)))))))))) (Rinv (IZR (Zpos (xO (xI (xO xH)))))))) (Rmult (IZR (Zpos (xO (xI (xO xH))))) (IZR (Zpos (xI (xO (xO (xO (xO xH)))))))) *)
prove_sup.
(* Goal: Rlt (IZR Z0) (v h) *)
(* Goal: Rlt (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH))))))))) (v h) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
apply TypeSpeed_pos.
(* Goal: Rlt (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH))))))))) (v h) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
apply Rlt_le_trans with MinSpeed.
(* Goal: Rlt (IZR (Zpos (xO (xO (xO (xI (xO (xO (xI xH))))))))) MinSpeed *)
(* Goal: Rle MinSpeed (v h) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
unfold MinSpeed in |- *; prove_sup.
(* Goal: Rle MinSpeed (v h) *)
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
apply (v_cond1 h).
(* Goal: Rlt (tan MaxBank) (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
apply Rlt_trans with tan_ub_MaxBank.
(* Goal: Rlt (tan MaxBank) tan_ub_MaxBank *)
(* Goal: Rlt tan_ub_MaxBank (IZR (Zpos xH)) *)
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
apply tan_MaxBank_ub.
unfold tan_ub_MaxBank in |- *; unfold Rdiv in |- *;
 apply Rmult_lt_reg_l with 10%R.
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO (xI (xO xH))))) *)
(* Goal: Rlt (Rmult (IZR (Zpos (xO (xI (xO xH))))) (Rmult (IZR (Zpos (xO (xI (xO (xO (xO (xO (xI (xO xH)))))))))) (Rinv (IZR (Zpos (xO (xI (xO xH)))))))) (Rmult (IZR (Zpos (xO (xI (xO xH))))) (IZR (Zpos (xI (xO (xO (xO (xO xH)))))))) *)
prove_sup.
rewrite <- Rmult_comm; rewrite Rmult_assoc; rewrite <- Rinv_l_sym;
 [ prove_sup | discrR ].
(* Goal: Rlt g (IZR (Zpos (xI (xO (xO (xO (xO xH))))))) *)
unfold g in |- *; unfold Rdiv in |- *; apply Rmult_lt_reg_l with 10%R.
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO (xI (xO xH))))) *)
(* Goal: Rlt (Rmult (IZR (Zpos (xO (xI (xO xH))))) (Rmult (IZR (Zpos (xO (xI (xO (xO (xO (xO (xI (xO xH)))))))))) (Rinv (IZR (Zpos (xO (xI (xO xH)))))))) (Rmult (IZR (Zpos (xO (xI (xO xH))))) (IZR (Zpos (xI (xO (xO (xO (xO xH)))))))) *)
prove_sup.
rewrite <- Rmult_comm; rewrite Rmult_assoc; rewrite <- Rinv_l_sym;
 [ prove_sup | discrR ].
Qed.

(**********)
Lemma rho_strict_decreasing :
 forall h1 h2 : TypeSpeed, (h1 < h2)%R -> (rho h2 < rho h1)%R.
intros; unfold rho in |- *; apply Rmult_lt_compat_l;
 [ apply g_pos
 | unfold Rdiv in |- *; apply Rmult_lt_compat_l;
    [ apply tan_MaxBank_pos
    | apply
       (Rinv_lt_contravar h1 h2
          (Rmult_lt_0_compat h1 h2 (TypeSpeed_pos h1) (TypeSpeed_pos h2)) H) ] ].
Qed.

(**********)
Lemma r_stric_increasing :
 forall h1 h2 : TypeSpeed, (h1 < h2)%R -> (r h1 < r h2)%R.
intros; unfold r in |- *; generalize (rho_strict_decreasing h1 h2 H);
 intro H0;
 generalize
  (Rinv_lt_contravar (rho h2) (rho h1)
     (Rmult_lt_0_compat (rho h2) (rho h1) (rho_pos h2) (rho_pos h1)) H0);
 intro;
 apply
  (Rmult_le_0_lt_compat h1 h2 (/ rho h1) (/ rho h2)
     (Rlt_le 0 h1 (TypeSpeed_pos h1))
     (Rlt_le 0 (/ rho h1) (Rinv_0_lt_compat (rho h1) (rho_pos h1))) H H1).
Qed.
