proposition: Lemma not_r_sum_rec : forall (A B S : Set) (l r : S), Not B -> forall H : A + B, sum_rec (fun _ : A + B => S) (fun x : A => l) (fun x : B => r) H = l.
proof: Proof. intros A B S l r H H0. elim H0. intro a. reflexivity. intro b. elim H. assumption. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)