proposition: Lemma int_negation_pred_negation_red x : - int_pred (- int_pred x) = x.
proof: Proof. destruct x as [x| |x]; trivial; destruct x; trivial; cbn; apply ap. 1: apply pos_pred_double_succ. rewrite pos_add_1_r. apply pos_succ_pred_double. Defined.
imports: Basics Spaces.Pos Spaces.Int.Core