Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
EApply ex3_2_intro;
Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
EApply ex3_2_intro;
(* case 3.2 : n = d0 *)
Rewrite H7; Rewrite H7 in H0; Clear H2 H7 n.
DropDis; Inversion H0; Rewrite H8 in H4; Clear H0 H7 H8 e u0.
(* case 3.2 : n = d0 *)
Rewrite H7; Rewrite H7 in H0; Clear H2 H7 n.
DropDis; Inversion H0; Rewrite H8 in H4; Clear H0 H7 H8 e u0.
Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
EApply ex3_2_intro;
Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
EApply ex3_2_intro;
LiftGen; Rewrite <- H0 in H2; Clear H0 x2.
Rewrite <- lift_d; [ Idtac | XAuto ].
Rewrite <- le_plus_minus; [ Idtac | XAuto ].
LiftGen; Rewrite <- H0 in H2; Clear H0 x2.
Rewrite <- lift_d; [ Idtac | XAuto ].
Rewrite <- le_plus_minus; [ Idtac | XAuto ].
LiftGen; Rewrite <- H0 in H2; Clear H0 x2.
Rewrite <- lift_d; [ Idtac | XAuto ].
Rewrite <- le_plus_minus; [ Idtac | XAuto ].
LiftGen; Rewrite <- H0 in H2; Clear H0 x2.
Rewrite <- lift_d; [ Idtac | XAuto ].
Rewrite <- le_plus_minus; [ Idtac | XAuto ].