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