proposition: Lemma int_pos_sub_negation a b : - (int_pos_sub a b) = int_pos_sub b a.
proof: Proof. revert a b. induction a as [|a ah|a ah]; destruct b; cbn; trivial. all: rewrite ?int_negation_double, ?int_negation_succ_double, ?int_negation_pred_double. all: apply ap, ah. Defined.
imports: Basics Spaces.Pos Spaces.Int.Core