proposition: Lemma addBnCAC m n p : n <= m -> n <= p -> m - n + p = p - n + m.
proof: Proof. by move=> nm np; rewrite addnC addnBA // subDnCA // addnC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring