proposition: Lemma not_r_cor_rect : forall (A B : CProp) (S : Type) (l r : S), Not B -> forall H : A or B, @sum_rect A B (fun _ : A or B => S) (fun x : A => l) (fun x : B => r) H = l.
proof: Proof. intros. elim H0. intros. reflexivity. intro. 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)