Require Export bord.

Section double_diagonale.

Notation rec4 := (Rec4 _ _ _ _ _) (only parsing).

Section definition.

Inductive DD : nat → nat → nat → Prop :=
  | DD_4 : ∀ t x : nat, quatre_end t x → DD t x trois
  | DD_5 : ∀ t x : nat, cinq_end t x → DD t x quatre
  | DD_A :
      ∀ t x cote : nat,
      six ≤ cote →
      Omod3 cote →
      A_basic t (x + pred (double (tiers cote))) (S (tiers cote)) →
      DD (t + S (tiers cote)) x (pred (double (tiers cote))) → DD t x cote
  | DD_B :
      ∀ t x cote : nat,
      sept ≤ cote →
      Unmod3 cote →
      B_basic t (x + double (tiers cote)) (S (tiers cote)) →
      DD (t + S (tiers cote)) x (double (tiers cote)) → DD t x cote
  | DD_C :
      ∀ t x cote : nat,
      cinq ≤ cote →
      Deuxmod3 cote →
      C_basic t (x + S (double (tiers cote))) (S (tiers cote)) →
      DD (t + S (tiers cote)) x (S (double (tiers cote))) → DD t x cote.

Lemma DD_GG :
 ∀ t x cote : nat,
 DD t x cote → G_Etat (t + cote) x ∧ G_Etat (S (t + cote)) x.
intros; elim H; intros.
rewrite plus_trois; apply quatre_GG; auto with v62.

rewrite plus_quatre; apply cinq_GG; auto with v62.

generalize H4.
rewrite plus_assoc_reverse; rewrite plus_Snm_nSm; rewrite <- S_pred.
rewrite (plus_comm (tiers cote0) (double (tiers cote0)));
 rewrite plus_deuxtiers_untiers; auto with v62.

apply lt_O_double; apply lt_O_tiers; apply le6_lt2; auto with v62.

generalize H4.
rewrite plus_assoc_reverse; rewrite plus_S.
rewrite (plus_comm (tiers cote0) (double (tiers cote0)));
 rewrite Splus_deuxtiers_untiers; auto with v62.

generalize H4.
rewrite plus_assoc_reverse; rewrite plus_S;
 rewrite <- (plus_n_Sm (tiers cote0)).
rewrite (plus_comm (tiers cote0) (double (tiers cote0)));
 rewrite SSplus_deuxtiers_untiers; auto with v62.
Qed.

End definition.

Section superposition.

Theorem DD_hh :
 ∀ t x cote : nat,
 DD t x cote →
 L_Etat (S (S t)) (x + cote) →
 L_Etat (S (S (S t))) (x + cote) → DD (S (S t)) x cote.
intros t x cote Hdd; elim Hdd; clear Hdd t x cote; intros.
rewrite (plus_trois x) in H0; rewrite (plus_trois x) in H1; apply DD_4;
 apply quatre_quatre; auto with v62.

rewrite (plus_quatre x) in H0; rewrite (plus_quatre x) in H1; apply DD_5;
 apply cinq_cinq; auto with v62.

apply (Rec4 _ _ _ _ _ (DD_A (S (S t)) x cote)); auto with v62.
clear H0; intros; apply A_A; auto with v62.
rewrite plus_assoc_reverse; rewrite <- plus_Snm_nSm; rewrite <- S_pred.
rewrite plus_deuxtiers_untiers; auto with v62.

apply lt_O_double; apply lt_O_tiers; apply le6_lt2; auto with v62.

rewrite plus_assoc_reverse; rewrite <- plus_Snm_nSm; rewrite <- S_pred.
rewrite plus_deuxtiers_untiers; auto with v62.

apply lt_O_double; apply lt_O_tiers; apply le6_lt2; auto with v62.

intros Ha; elim Ha; clear Ha; intros; apply H3.
elim H7; auto with v62.

elim H8; auto with v62.

apply (Rec4 _ _ _ _ _ (DD_B (S (S t)) x cote)); auto with v62.
intros; apply B_B; auto with v62.
rewrite plus_assoc_reverse; rewrite <- plus_n_Sm;
 rewrite Splus_deuxtiers_untiers; auto with v62.

rewrite plus_assoc_reverse; rewrite <- plus_n_Sm;
 rewrite Splus_deuxtiers_untiers; auto with v62.

intros Hb; elim Hb; clear Hb; intros; apply H3.
elim H7; auto with v62.

elim H8; auto with v62.

apply (Rec4 _ _ _ _ _ (DD_C (S (S t)) x cote)); auto with v62.
intros; apply C_C; auto with v62.
rewrite plus_assoc_reverse; rewrite <- plus_n_Sm; simpl in |- *;
 rewrite SSplus_deuxtiers_untiers; auto with v62.

rewrite plus_assoc_reverse; rewrite <- plus_n_Sm; simpl in |- *;
 rewrite SSplus_deuxtiers_untiers; auto with v62.

intros Hc; elim Hc; clear Hc; intros; apply H3.
elim H7; auto with v62.

elim H8; auto with v62.
Qed.

Theorem DD_hddollar :
 ∀ t x cote : nat,
 DD t x cote →
 L_Etat (S t) (x + S cote) →
 L_Etat (S (S t)) (x + S cote) → DD (S t) x (S cote).
intros t x cote Hdd; elim Hdd; clear Hdd t x cote; intros.
apply DD_5; apply quatre_cinq; auto with v62.
generalize H0; rewrite plus_quatre; auto with v62.

generalize H1; rewrite plus_quatre; auto with v62.

apply DD_C; auto with v62.
unfold Deuxmod3 in |- *; auto with v62.

unfold tiers, double in |- *; simpl in |- *; elim (cinq_quatre t x);
 auto with v62.

unfold tiers, double in |- *; simpl in |- *; rewrite plus_deux; apply DD_4;
 elim (cinq_quatre t x); auto with v62.

cut (0 < double (tiers cote)); intros.
apply (Rec4 _ _ _ _ _ (DD_B (S t) x (S cote))); try rewrite <- (tiers_S cote);
 try rewrite (S_pred (double (tiers cote))); auto with v62.
unfold sept in |- *; apply le_n_S; auto with v62.

apply Omod3_Unmod3; auto with v62.

intro; rewrite <- plus_n_Sm; apply A_B; auto with v62.
rewrite plus_n_Sm; rewrite <- S_pred; auto with v62.
rewrite plus_assoc_reverse; rewrite <- plus_n_Sm;
 rewrite plus_deuxtiers_untiers; auto with v62.

rewrite plus_n_Sm; rewrite <- S_pred; auto with v62.
rewrite plus_assoc_reverse; rewrite <- plus_n_Sm;
 rewrite plus_deuxtiers_untiers; auto with v62.

intros Hb; elim Hb; clear Hb; intros; apply H3.
elim H8; auto with v62.

elim H9; auto with v62.

apply lt_O_double; apply lt_O_tiers; apply le6_lt2; auto with v62.

apply (Rec4 _ _ _ _ _ (DD_C (S t) x (S cote)));
 try rewrite <- (tiers_SS cote); auto with v62.
unfold cinq in |- *; apply le_n_S; apply le_trans with (m := 7);
 auto with v62.

apply Unmod3_Deuxmod3; auto with v62.

intro; rewrite <- plus_n_Sm; apply B_C; auto with v62.
rewrite plus_n_Sm; rewrite plus_assoc_reverse; rewrite <- plus_n_Sm;
 simpl in |- *; rewrite Splus_deuxtiers_untiers; auto with v62.

rewrite plus_n_Sm; rewrite plus_assoc_reverse; rewrite <- plus_n_Sm;
 simpl in |- *; rewrite Splus_deuxtiers_untiers; auto with v62.

intros Hc; elim Hc; clear Hc; intros; apply H3.
elim H7; auto with v62.

elim H8; auto with v62.

apply (Rec4 _ _ _ _ _ (DD_A (S t) x (S cote)));
 try rewrite <- (tiers_SSS cote); auto with v62.
unfold six in |- *; apply le_n_S; auto with v62.

apply Deuxmod3_Omod3; auto with v62.

intro; rewrite double_S; apply C_A; auto with v62.
simpl in |- *; rewrite plus_assoc_reverse; rewrite <- plus_Snm_nSm;
 rewrite <- double_S; rewrite tiers_SSS; auto with v62;
 rewrite plus_deuxtiers_untiers; auto with v62.

simpl in |- *; rewrite plus_assoc_reverse; rewrite <- plus_Snm_nSm;
 rewrite <- double_S; rewrite tiers_SSS; auto with v62;
 rewrite plus_deuxtiers_untiers; auto with v62.

rewrite double_S; simpl in |- *; intros Ha; elim Ha; clear Ha; intros;
 rewrite <- plus_n_Sm; apply DD_hh; auto with v62.
rewrite plus_n_Sm; elim H7; auto with v62.

rewrite plus_n_Sm; elim H8; auto with v62.
Qed.

End superposition.

End double_diagonale.